:: RELSET_1 semantic presentation begin definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; mode Relation of "X" "," "Y" is ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_relat_1 :::"Relation-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster -> "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "Z" be ($#m1_hidden :::"set"::: ) ; :: original: :::"c="::: redefine pred "R" :::"c="::: "Z" means :: RELSET_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "Z"))); end; :: deftheorem defines :::"c="::: RELSET_1:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set (Var "Z"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))))) ")" )))); definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "P", "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"="::: redefine pred "P" :::"="::: "R" means :: RELSET_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "P") "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ))); end; :: deftheorem defines :::"="::: RELSET_1:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ))) ")" ))); theorem :: RELSET_1:1 (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: RELSET_1:2 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )))) ; theorem :: RELSET_1:3 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ; theorem :: RELSET_1:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: RELSET_1:5 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X1")))) "holds" (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))))) ; theorem :: RELSET_1:6 (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y1")))) "holds" (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y1"))))) ; theorem :: RELSET_1:7 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "Y")) "," (Set (Var "Y1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "X1"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1")))) "holds" (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X1")) "," (Set (Var "Y1"))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R", "S" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R", "S" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> "X" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> "X" ($#v5_relat_1 :::"-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> "X" ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); :: original: :::"dom"::: redefine func :::"dom"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); :: original: :::"rng"::: redefine func :::"rng"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: RELSET_1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))))) ; theorem :: RELSET_1:9 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ) "iff" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: RELSET_1:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ) "iff" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" ))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"~"::: redefine func "R" :::"~"::: -> ($#m1_subset_1 :::"Relation":::) "of" "Y" "," "X"; end; definitionlet "X", "Y1", "Y2", "Z" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y1")); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "Y2")) "," (Set (Const "Z")); :: original: :::"*"::: redefine func "P" :::"*"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" "X" "," "Z"; end; theorem :: RELSET_1:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "R")) ($#k3_relset_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) ")" ))) ; theorem :: RELSET_1:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ; registrationlet "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) )); cluster -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "A" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: RELSET_1:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: RELSET_1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "X")))) ; theorem :: RELSET_1:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) ")" ))) ; theorem :: RELSET_1:16 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) ")" ))) ; theorem :: RELSET_1:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) ")" ))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "A" be ($#m1_hidden :::"set"::: ) ; :: original: :::"|"::: redefine func "R" :::"|"::: "A" -> ($#m1_subset_1 :::"Relation":::) "of" "X" "," "Y"; end; definitionlet "X", "Y", "B" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"|`"::: redefine func "B" :::"|`"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" "X" "," "Y"; end; theorem :: RELSET_1:18 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "R")) ($#k5_relset_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))))) ; theorem :: RELSET_1:19 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "X1")))) "holds" (Bool (Set (Set (Var "R")) ($#k5_relset_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))))) ; theorem :: RELSET_1:20 (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "Y1")) ($#k6_relset_1 :::"|`"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y1"))))) ; theorem :: RELSET_1:21 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Y1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1")))) "holds" (Bool (Set (Set (Var "Y1")) ($#k6_relset_1 :::"|`"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "A" be ($#m1_hidden :::"set"::: ) ; :: original: :::".:"::: redefine func "R" :::".:"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "Y"; :: original: :::"""::: redefine func "R" :::"""::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: RELSET_1:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "R")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) ")" ))) ; theorem :: RELSET_1:23 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "R")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "R")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) ")" ))) ; scheme :: RELSET_1:sch 1 RelOnSetEx{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ))) proof end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Relation of "X" is ($#m1_subset_1 :::"Relation":::) "of" "X" "," "X"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: RELSET_1:24 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" )))) ; theorem :: RELSET_1:25 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" )))) ; theorem :: RELSET_1:26 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R"))))))) ; theorem :: RELSET_1:27 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R"))))))) ; theorem :: RELSET_1:28 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "E")) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k4_relset_1 :::"*"::: ) (Set (Var "R")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ")" ))))) ; theorem :: RELSET_1:29 (Bool "for" (Set (Var "E")) "," (Set (Var "D1")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D1")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D1"))) ")" )) ")" )))) ; theorem :: RELSET_1:30 (Bool "for" (Set (Var "D")) "," (Set (Var "D2")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k8_relset_1 :::"""::: ) (Set (Var "D2")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D2"))) ")" )) ")" )))) ; scheme :: RELSET_1:sch 2 RelOnDomEx{ 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_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" )))) proof end; begin scheme :: RELSET_1:sch 3 Sch3{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) ")" )))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set F3 "(" (Set (Var "i")) ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" ))) proof end; theorem :: RELSET_1:31 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "N")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" )) ")" )) "holds" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Var "S"))))) ; scheme :: RELSET_1:sch 4 Sch4{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F3() -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) } : (Bool (Set F3 "(" ")" ) ($#r2_relset_1 :::"="::: ) (Set F4 "(" ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "iff" (Bool P1[(Set (Var "p")) "," (Set (Var "q"))]) ")" ))) and (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set F4 "(" ")" )) "iff" (Bool P1[(Set (Var "p")) "," (Set (Var "q"))]) ")" ))) proof end; registrationlet "X", "Y", "Z" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "Z")); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "f") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "X", "Y", "Z" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "Y")) "," (Set (Const "Z")) ($#k2_zfmisc_1 :::":]"::: ) ); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "f") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; theorem :: RELSET_1:32 (Bool "for" (Set (Var "Y")) "," (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "P")) ($#k5_relset_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; registrationlet "R" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::); let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "R")) ")" ); cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "Y") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "R" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::); let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "R")) ")" ); cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "Y") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end;