:: FRAENKEL semantic presentation begin scheme :: FRAENKEL:sch 1 Fraenkel59{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "v")) ")" ) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v"))]) "}" ($#r1_tarski :::"c="::: ) "{" (Set F2 "(" (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P2[(Set (Var "u"))]) "}" ) provided (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "v"))])) "holds" (Bool P2[(Set (Var "v"))])) proof end; scheme :: FRAENKEL:sch 2 Fraenkel599{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) where u1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "u1")) "," (Set (Var "v1"))]) "}" ($#r1_tarski :::"c="::: ) "{" (Set F3 "(" (Set (Var "u2")) "," (Set (Var "v2")) ")" ) where u2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P2[(Set (Var "u2")) "," (Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "u")) "," (Set (Var "v"))])) "holds" (Bool P2[(Set (Var "u")) "," (Set (Var "v"))]))) proof end; scheme :: FRAENKEL:sch 3 Fraenkel69{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "v1")) ")" ) where v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F2 "(" (Set (Var "v2")) ")" ) where v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P2[(Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "v"))]) "iff" (Bool P2[(Set (Var "v"))]) ")" )) proof end; scheme :: FRAENKEL:sch 4 Fraenkel699{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) where u1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "u1")) "," (Set (Var "v1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "u2")) "," (Set (Var "v2")) ")" ) where u2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P2[(Set (Var "u2")) "," (Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "u")) "," (Set (Var "v"))]) "iff" (Bool P2[(Set (Var "u")) "," (Set (Var "v"))]) ")" ))) proof end; scheme :: FRAENKEL:sch 5 FraenkelF9{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "v1")) ")" ) where v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "v2")) ")" ) where v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F2 "(" (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "v")) ")" ))) proof end; scheme :: FRAENKEL:sch 6 FraenkelF9R{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "v1")) ")" ) where v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "v2")) ")" ) where v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "v"))])) "holds" (Bool (Set F2 "(" (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "v")) ")" ))) proof end; scheme :: FRAENKEL:sch 7 FraenkelF99{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) where u1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "u1")) "," (Set (Var "v1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "u2")) "," (Set (Var "v2")) ")" ) where u2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "u2")) "," (Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set F3 "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "u")) "," (Set (Var "v")) ")" )))) proof end; scheme :: FRAENKEL:sch 8 FraenkelF699{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) where u1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "u1")) "," (Set (Var "v1"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "v2")) "," (Set (Var "u2")) ")" ) where u2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P2[(Set (Var "u2")) "," (Set (Var "v2"))]) "}" ) provided (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "u")) "," (Set (Var "v"))]) "iff" (Bool P2[(Set (Var "u")) "," (Set (Var "v"))]) ")" ))) and (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set F3 "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "v")) "," (Set (Var "u")) ")" )))) proof end; theorem :: FRAENKEL:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: FRAENKEL:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FRAENKEL:3 (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "A")) "," (Set (Var "B")))))) ; scheme :: FRAENKEL:sch 9 RelevantArgs{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "u9")) ")" ) where u9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool P1[(Set (Var "u9"))]) & (Bool (Set (Var "u9")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v9")) ")" ) where v9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool P2[(Set (Var "v9"))]) & (Bool (Set (Var "v9")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) ")" ) "}" ) provided (Bool (Set (Set F4 "(" ")" ) ($#k2_partfun1 :::"|"::: ) (Set F3 "(" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set F5 "(" ")" ) ($#k2_partfun1 :::"|"::: ) (Set F3 "(" ")" ))) and (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "(" (Bool P1[(Set (Var "u"))]) "iff" (Bool P2[(Set (Var "u"))]) ")" )) proof end; scheme :: FRAENKEL:sch 10 FrSet0{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) proof end; scheme :: FRAENKEL:sch 11 Gen199{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "s")) "," (Set (Var "t"))])) "holds" (Bool P2[(Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" )]))) provided (Bool "for" (Set (Var "st1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "st1")) ($#r2_hidden :::"in"::: ) "{" (Set F3 "(" (Set (Var "s1")) "," (Set (Var "t1")) ")" ) where s1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "s1")) "," (Set (Var "t1"))]) "}" )) "holds" (Bool P2[(Set (Var "st1"))])) proof end; scheme :: FRAENKEL:sch 12 Gen199A{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "st1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "st1")) ($#r2_hidden :::"in"::: ) "{" (Set F3 "(" (Set (Var "s1")) "," (Set (Var "t1")) ")" ) where s1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "s1")) "," (Set (Var "t1"))]) "}" )) "holds" (Bool P2[(Set (Var "st1"))])) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "s")) "," (Set (Var "t"))])) "holds" (Bool P2[(Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" )]))) proof end; scheme :: FRAENKEL:sch 13 Gen299{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set (Var "st1")) where st1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) : (Bool "(" (Bool (Set (Var "st1")) ($#r2_hidden :::"in"::: ) "{" (Set F4 "(" (Set (Var "s1")) "," (Set (Var "t1")) ")" ) where s1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "s1")) "," (Set (Var "t1"))]) "}" ) & (Bool P2[(Set (Var "st1"))]) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "s2")) "," (Set (Var "t2")) ")" ) where s2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool "(" (Bool P1[(Set (Var "s2")) "," (Set (Var "t2"))]) & (Bool P2[(Set F4 "(" (Set (Var "s2")) "," (Set (Var "t2")) ")" )]) ")" ) "}" ) proof end; scheme :: FRAENKEL:sch 14 Gen39{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "s")) ")" ) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "{" (Set (Var "s1")) where s1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P2[(Set (Var "s1"))]) "}" ) & (Bool P1[(Set (Var "s"))]) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set F2 "(" (Set (Var "s2")) ")" ) where s2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool P2[(Set (Var "s2"))]) & (Bool P1[(Set (Var "s2"))]) ")" ) "}" ) proof end; scheme :: FRAENKEL:sch 15 Gen399{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "{" (Set (Var "s1")) where s1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P2[(Set (Var "s1"))]) "}" ) & (Bool P1[(Set (Var "s")) "," (Set (Var "t"))]) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "s2")) "," (Set (Var "t2")) ")" ) where s2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool "(" (Bool P2[(Set (Var "s2"))]) & (Bool P1[(Set (Var "s2")) "," (Set (Var "t2"))]) ")" ) "}" ) proof end; scheme :: FRAENKEL:sch 16 Gen499{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "s")) "," (Set (Var "t"))]) "}" ($#r1_tarski :::"c="::: ) "{" (Set F3 "(" (Set (Var "s1")) "," (Set (Var "t1")) ")" ) where s1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P2[(Set (Var "s1")) "," (Set (Var "t1"))]) "}" ) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "s")) "," (Set (Var "t"))])) "holds" (Bool "ex" (Set (Var "s9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool P2[(Set (Var "s9")) "," (Set (Var "t"))]) & (Bool (Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "s9")) "," (Set (Var "t")) ")" )) ")" )))) proof end; scheme :: FRAENKEL:sch 17 FrSet1{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool (Set F3 "(" (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "y"))]) ")" ) "}" ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) proof end; scheme :: FRAENKEL:sch 18 FrSet2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool P1[(Set (Var "y"))]) & (Bool (Bool "not" (Set F3 "(" (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) ")" ) "}" ($#r1_xboole_0 :::"misses"::: ) (Set F2 "(" ")" )) proof end; scheme :: FRAENKEL:sch 19 FrEqua1{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P2[(Set (Var "s")) "," (Set (Var "t"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "s9")) "," (Set F4 "(" ")" ) ")" ) where s9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "s9")) "," (Set F4 "(" ")" )]) "}" ) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool P2[(Set (Var "s")) "," (Set (Var "t"))]) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool P1[(Set (Var "s")) "," (Set (Var "t"))]) ")" ) ")" ))) proof end; scheme :: FRAENKEL:sch 20 FrEqua2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool P1[(Set (Var "s")) "," (Set (Var "t"))]) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "s9")) "," (Set F4 "(" ")" ) ")" ) where s9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "s9")) "," (Set F4 "(" ")" )]) "}" ) proof end; theorem :: FRAENKEL:4 (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) (Bool "ex" (Set (Var "phi")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "st" (Bool (Set (Set (Var "phi")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))))) ; theorem :: FRAENKEL:5 (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "phi")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "holds" (Bool (Set (Set (Var "phi")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "phi")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")) ")" )))))) ; scheme :: FRAENKEL:sch 21 FraenkelFin{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) provided (Bool (Set F2 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; scheme :: FRAENKEL:sch 22 CartFin{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F5 "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set F4 "(" ")" )) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) provided (Bool (Set F3 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool (Set F4 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; scheme :: FRAENKEL:sch 23 Finiteness{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )), P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )] } : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "z")) "," (Set (Var "y"))])) "holds" (Bool P1[(Set (Var "y")) "," (Set (Var "z"))]) ")" ) ")" ))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "x"))])) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) proof end; scheme :: FRAENKEL:sch 24 FinIm{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F2 "(" ")" )), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "c1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) "st" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "c1"))) "iff" (Bool "ex" (Set (Var "t9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "t9")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "t9")) ")" )) & (Bool P1[(Set (Var "t")) "," (Set (Var "t9"))]) ")" )) ")" ))) proof end; registrationlet "A", "B" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "A" "," "B" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FRAENKEL:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#v1_finset_1 :::"finite"::: ) )) ; scheme :: FRAENKEL:sch 25 ImFin{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F5 "(" (Set (Var "phi9")) ")" ) where phi9 "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ")" ) : (Bool (Set (Set (Var "phi9")) ($#k7_relset_1 :::".:"::: ) (Set F3 "(" ")" )) ($#r1_tarski :::"c="::: ) (Set F4 "(" ")" )) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) provided (Bool (Set F3 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool (Set F4 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool "for" (Set (Var "phi")) "," (Set (Var "psi")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ")" ) "st" (Bool (Bool (Set (Set (Var "phi")) ($#k2_partfun1 :::"|"::: ) (Set F3 "(" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "psi")) ($#k2_partfun1 :::"|"::: ) (Set F3 "(" ")" )))) "holds" (Bool (Set F5 "(" (Set (Var "phi")) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "psi")) ")" ))) proof end; scheme :: FRAENKEL:sch 26 FunctChoice{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )], F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) } : (Bool "ex" (Set (Var "ff")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool P1[(Set (Var "t")) "," (Set (Set (Var "ff")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))]))) provided (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "ex" (Set (Var "ff")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool P1[(Set (Var "t")) "," (Set (Var "ff"))]))) proof end; scheme :: FRAENKEL:sch 27 FuncsChoice{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )], F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) } : (Bool "ex" (Set (Var "ff")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ")" ) "st" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool P1[(Set (Var "t")) "," (Set (Set (Var "ff")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))]))) provided (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "ex" (Set (Var "ff")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool P1[(Set (Var "t")) "," (Set (Var "ff"))]))) proof end; scheme :: FRAENKEL:sch 28 FraenkelFin9{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool P1[(Set (Var "w")) "," (Set (Var "x"))]) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) ")" )) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) provided (Bool (Set F3 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "w")) "," (Set (Var "x"))]) & (Bool P1[(Set (Var "w")) "," (Set (Var "y"))])) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) proof end;