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