environ
vocabularies HIDDEN, XBOOLE_0, TARSKI, SUBSET_1, RELAT_2, ORDERS_2, WAYBEL_0, YELLOW_1, CARD_FIL, STRUCT_0, ZFMISC_1, XXREAL_0, LATTICE3, ORDINAL2, YELLOW_0, LATTICES, WAYBEL_2, YELLOW_9, WAYBEL11, REWRITE1, WAYBEL_9, PRE_TOPC, PROB_1, WAYBEL19, PRELAMB, ORDINAL1, SETFAM_1, CANTOR_1, DIRAF, RCOMP_1, FINSET_1, RLVECT_3, COMPTS_1, YELLOW_8, TOPS_1, WAYBEL29, YELLOW13, FUNCT_1, WAYBEL21, RELAT_1, PARTFUN1, MCART_1, TOPS_2, WAYBEL_3, TDLAT_3, CONNSP_2, EQREL_1, WAYBEL_8, WAYBEL_6, WAYBEL30, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, BINOP_1, FUNCT_3, SETFAM_1, DOMAIN_1, CARD_1, STRUCT_0, FINSET_1, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, TDLAT_3, LATTICE3, BORSUK_1, CANTOR_1, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL_6, WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29;
definitions TARSKI, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL19, WAYBEL11, YELLOW13, XBOOLE_0, TOPS_2;
theorems TARSKI, PRE_TOPC, ORDERS_2, TOPS_1, TOPS_2, BORSUK_1, CONNSP_2, TDLAT_3, COMPTS_1, RELAT_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, YELLOW_8, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_8, YELLOW13, WAYBEL11, WAYBEL12, WAYBEL14, YELLOW_9, WAYBEL19, YELLOW12, WAYBEL21, WAYBEL29, SETFAM_1, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes SUBSET_1, FINSET_1, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TEX_1, WAYBEL_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, YELLOW_6, WAYBEL_8, WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, YELLOW12, WAYBEL19, YELLOW13, PRE_TOPC, CARD_1;
constructors HIDDEN, TOPS_1, TOPS_2, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29, COMPTS_1, WAYBEL_2;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities LATTICE3, WAYBEL_0, WAYBEL_3, WAYBEL11, BINOP_1, STRUCT_0;
expansions TARSKI, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_3, WAYBEL11, YELLOW13, XBOOLE_0;
Lm3:
now for S, T, x1, x2 being set st x1 in S & x2 in T holds
<:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]
let S,
T,
x1,
x2 be
set ;
( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1] )assume that A1:
x1 in S
and A2:
x2 in T
;
<:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]A3:
dom <:(pr2 (S,T)),(pr1 (S,T)):> =
(dom (pr2 (S,T))) /\ (dom (pr1 (S,T)))
by FUNCT_3:def 7
.=
(dom (pr2 (S,T))) /\ [:S,T:]
by FUNCT_3:def 4
.=
[:S,T:] /\ [:S,T:]
by FUNCT_3:def 5
.=
[:S,T:]
;
[x1,x2] in [:S,T:]
by A1, A2, ZFMISC_1:87;
hence <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] =
[((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))]
by A3, FUNCT_3:def 7
.=
[x2,((pr1 (S,T)) . (x1,x2))]
by A1, A2, FUNCT_3:def 5
.=
[x2,x1]
by A1, A2, FUNCT_3:def 4
;
verum
end;