let F, H be ZF-formula; for x, y being Variable holds
( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
let x, y be Variable; ( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
set N = ('not' H) / (x,y);
A1:
len <*2*> = 1
by FINSEQ_1:39;
A2:
( dom ('not' F) = Seg (len ('not' F)) & dom ('not' H) = Seg (len ('not' H)) )
by FINSEQ_1:def 3;
A3:
( len ('not' F) = (len <*2*>) + (len F) & len ('not' H) = (len <*2*>) + (len H) )
by FINSEQ_1:22;
A4:
( dom F = Seg (len F) & dom H = Seg (len H) )
by FINSEQ_1:def 3;
thus
( 'not' F = ('not' H) / (x,y) implies F = H / (x,y) )
( F = H / (x,y) implies 'not' F = ('not' H) / (x,y) )proof
assume A5:
'not' F = ('not' H) / (
x,
y)
;
F = H / (x,y)
then A6:
dom ('not' F) = dom ('not' H)
by Def3;
then A7:
len ('not' F) = len ('not' H)
by FINSEQ_3:29;
A8:
now for a being object st a in dom F holds
F . a = (H / (x,y)) . alet a be
object ;
( a in dom F implies F . a = (H / (x,y)) . a )assume A9:
a in dom F
;
F . a = (H / (x,y)) . athen reconsider i =
a as
Element of
NAT ;
A10:
(
F . a = (('not' H) / (x,y)) . (1 + i) & 1
+ i in dom (('not' H) / (x,y)) )
by A1, A5, A9, FINSEQ_1:28, FINSEQ_1:def 7;
A11:
('not' H) . (1 + i) = H . a
by A1, A4, A3, A7, A9, FINSEQ_1:def 7;
then A12:
(
H . a = x implies
F . a = y )
by A5, A6, A10, Def3;
A13:
(
H . a <> x implies
F . a = H . a )
by A5, A6, A10, A11, Def3;
(
H . a = x implies
(H / (x,y)) . a = y )
by A4, A3, A7, A9, Def3;
hence
F . a = (H / (x,y)) . a
by A4, A3, A7, A9, A12, A13, Def3;
verum end;
A14:
dom H = dom (H / (x,y))
by Def3;
dom F = dom H
by A3, A7, FINSEQ_3:29;
hence
F = H / (
x,
y)
by A14, A8, FUNCT_1:2;
verum
end;
assume A15:
F = H / (x,y)
; 'not' F = ('not' H) / (x,y)
then A16:
dom F = dom H
by Def3;
then A17:
len F = len H
by FINSEQ_3:29;
A18:
dom <*2*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
A19:
now for a being object st a in dom ('not' F) holds
('not' F) . a = (('not' H) / (x,y)) . alet a be
object ;
( a in dom ('not' F) implies ('not' F) . a = (('not' H) / (x,y)) . a )assume A20:
a in dom ('not' F)
;
('not' F) . a = (('not' H) / (x,y)) . athen reconsider i =
a as
Element of
NAT ;
A21:
now ( ex j being Nat st
( j in dom F & i = 1 + j ) implies ('not' F) . a = (('not' H) / (x,y)) . a )A22:
(
('not' H) . a <> x implies
(('not' H) / (x,y)) . a = ('not' H) . a )
by A2, A3, A17, A20, Def3;
given j being
Nat such that A23:
j in dom F
and A24:
i = 1
+ j
;
('not' F) . a = (('not' H) / (x,y)) . aA25:
(
H . j = ('not' H) . i &
F . j = ('not' F) . i )
by A1, A16, A23, A24, FINSEQ_1:def 7;
then A26:
(
('not' H) . a = x implies
('not' F) . a = y )
by A15, A16, A23, Def3;
(
('not' H) . a <> x implies
('not' F) . a = ('not' H) . a )
by A15, A16, A23, A25, Def3;
hence
('not' F) . a = (('not' H) / (x,y)) . a
by A2, A3, A17, A20, A26, A22, Def3;
verum end; hence
('not' F) . a = (('not' H) / (x,y)) . a
by A1, A18, A20, A21, FINSEQ_1:25;
verum end;
dom ('not' F) = dom (('not' H) / (x,y))
by A2, A3, A17, Def3;
hence
'not' F = ('not' H) / (x,y)
by A19, FUNCT_1:2; verum