let x1, x2, y1, y2, z1, z2 be Variable; :: thesis: ( (x1 'in' x2) / (y1,y2) = z1 'in' z2 iff ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )
set H = x1 'in' x2;
set Hz = z1 'in' z2;
set f = (x1 'in' x2) / (y1,y2);
A1: ( (x1 'in' x2) . 1 = 1 & y1 <> 1 ) by Th135, ZF_LANG:15;
x1 'in' x2 is being_membership ;
then A2: x1 'in' x2 is atomic ;
then A3: len (x1 'in' x2) = 3 by ZF_LANG:11;
then A4: dom (x1 'in' x2) = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
z1 'in' z2 is being_membership ;
then A5: z1 'in' z2 is atomic ;
then len (z1 'in' z2) = 3 by ZF_LANG:11;
then A6: dom (z1 'in' z2) = Seg 3 by FINSEQ_1:def 3;
Var1 (z1 'in' z2) = z1 by Th2;
then A7: (z1 'in' z2) . 2 = z1 by A5, ZF_LANG:35;
Var2 (z1 'in' z2) = z2 by Th2;
then A8: (z1 'in' z2) . 3 = z2 by A5, ZF_LANG:35;
A9: Var2 (x1 'in' x2) = x2 by Th2;
then A10: (x1 'in' x2) . 3 = x2 by A2, ZF_LANG:35;
A11: Var1 (x1 'in' x2) = x1 by Th2;
then A12: (x1 'in' x2) . 2 = x1 by A2, ZF_LANG:35;
thus ( not (x1 'in' x2) / (y1,y2) = z1 'in' z2 or ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) :: thesis: ( ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 )
proof
assume A13: (x1 'in' x2) / (y1,y2) = z1 'in' z2 ; :: thesis: ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) )
per cases ( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;
case A14: ( x1 <> y1 & x2 <> y1 ) ; :: thesis: ( z1 = x1 & z2 = x2 )
( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def 1;
hence ( z1 = x1 & z2 = x2 ) by A12, A10, A7, A8, A13, A14, Def3; :: thesis: verum
end;
case A15: ( x1 = y1 & x2 <> y1 ) ; :: thesis: ( z1 = y2 & z2 = x2 )
A16: ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def 1;
(x1 'in' x2) . 2 = y1 by A2, A11, A15, ZF_LANG:35;
hence ( z1 = y2 & z2 = x2 ) by A10, A7, A8, A13, A15, A16, Def3; :: thesis: verum
end;
case A17: ( x1 <> y1 & x2 = y1 ) ; :: thesis: ( z1 = x1 & z2 = y2 )
A18: ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def 1;
(x1 'in' x2) . 3 = y1 by A2, A9, A17, ZF_LANG:35;
hence ( z1 = x1 & z2 = y2 ) by A12, A7, A8, A13, A17, A18, Def3; :: thesis: verum
end;
case A19: ( x1 = y1 & x2 = y1 ) ; :: thesis: ( z1 = y2 & z2 = y2 )
A20: ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def 1;
( (x1 'in' x2) . 2 = y1 & (x1 'in' x2) . 3 = y1 ) by A2, A11, A9, A19, ZF_LANG:35;
hence ( z1 = y2 & z2 = y2 ) by A7, A8, A13, A20, Def3; :: thesis: verum
end;
end;
end;
A21: dom (x1 'in' x2) = Seg 3 by A3, FINSEQ_1:def 3;
A22: dom ((x1 'in' x2) / (y1,y2)) = dom (x1 'in' x2) by Def3;
A23: now :: thesis: ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 )
assume A24: ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) ; :: thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now :: thesis: for a being object st a in dom (x1 'in' x2) holds
(z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
let a be object ; :: thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A25: a in dom (x1 'in' x2) ; :: thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def 1;
hence (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A1, A24, A25, Def3; :: thesis: verum
end;
hence (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; :: thesis: verum
end;
A26: (z1 'in' z2) . 1 = 1 by ZF_LANG:15;
A27: now :: thesis: ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 )
assume A28: ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) ; :: thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now :: thesis: for a being object st a in dom (x1 'in' x2) holds
(z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
let a be object ; :: thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A29: a in dom (x1 'in' x2) ; :: thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def 1;
hence (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A28, A29, Def3; :: thesis: verum
end;
hence (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; :: thesis: verum
end;
A30: now :: thesis: ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 )
assume A31: ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ; :: thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now :: thesis: for a being object st a in dom (x1 'in' x2) holds
(z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
let a be object ; :: thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A32: a in dom (x1 'in' x2) ; :: thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def 1;
hence (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A31, A32, Def3; :: thesis: verum
end;
hence (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; :: thesis: verum
end;
now :: thesis: ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 )
assume A33: ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) ; :: thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now :: thesis: for a being object st a in dom (x1 'in' x2) holds
(z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
let a be object ; :: thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A34: a in dom (x1 'in' x2) ; :: thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def 1;
hence (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A33, A34, Def3; :: thesis: verum
end;
hence (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; :: thesis: verum
end;
hence ( ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 ) by A23, A27, A30; :: thesis: verum