let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: B ^ C = C ^ B
deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
defpred S1[ set , set ] means ( $1 in B & $2 in C );
defpred S2[ set , set ] means ( $2 in C & $1 in B );
set X1 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } ;
set X2 = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } ;
A1:
for s, t being Element of DISJOINT_PAIRS A holds
( S1[s,t] iff S2[s,t] )
;
A2:
for s, t being Element of DISJOINT_PAIRS A holds H1(s,t) = H1(t,s)
;
A3:
{ H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] }
from FRAENKEL:sch 8(A1, A2);
now let x be
set ;
:: thesis: ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )
(
x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex
s,
t being
Element of
DISJOINT_PAIRS A st
(
x = t \/ s &
t in C &
s in B ) )
;
then
(
x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex
t,
s being
Element of
DISJOINT_PAIRS A st
(
x = t \/ s &
t in C &
s in B ) )
;
hence
(
x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff
x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )
;
:: thesis: verum end;
hence
B ^ C = C ^ B
by A3, TARSKI:2; :: thesis: verum