let V be non empty set ; Maps V = union { (Maps (A,B)) where A, B is Element of V : verum }
set M = { (Maps (A,B)) where A, B is Element of V : verum } ;
now for z being object holds
( ( z in Maps V implies z in union { (Maps (A,B)) where A, B is Element of V : verum } ) & ( z in union { (Maps (A,B)) where A, B is Element of V : verum } implies z in Maps V ) )let z be
object ;
( ( z in Maps V implies z in union { (Maps (A,B)) where A, B is Element of V : verum } ) & ( z in union { (Maps (A,B)) where A, B is Element of V : verum } implies z in Maps V ) )thus
(
z in Maps V implies
z in union { (Maps (A,B)) where A, B is Element of V : verum } )
( z in union { (Maps (A,B)) where A, B is Element of V : verum } implies z in Maps V )proof
assume
z in Maps V
;
z in union { (Maps (A,B)) where A, B is Element of V : verum }
then consider f being
Element of
Funcs V,
A,
B being
Element of
V such that A1:
(
z = [[A,B],f] & (
B = {} implies
A = {} ) &
f is
Function of
A,
B )
by Th4;
A2:
Maps (
A,
B)
in { (Maps (A,B)) where A, B is Element of V : verum }
;
z in Maps (
A,
B)
by A1, Th15;
hence
z in union { (Maps (A,B)) where A, B is Element of V : verum }
by A2, TARSKI:def 4;
verum
end; assume
z in union { (Maps (A,B)) where A, B is Element of V : verum }
;
z in Maps Vthen consider C being
set such that A3:
z in C
and A4:
C in { (Maps (A,B)) where A, B is Element of V : verum }
by TARSKI:def 4;
consider A,
B being
Element of
V such that A5:
C = Maps (
A,
B)
by A4;
ex
f being
Element of
Funcs V st
(
z = [[A,B],f] &
[[A,B],f] in Maps V )
by A3, A5;
hence
z in Maps V
;
verum end;
hence
Maps V = union { (Maps (A,B)) where A, B is Element of V : verum }
by TARSKI:2; verum