Step | Hyp | Ref | Expression |
1 |
|
hyp hn |
x = n -> (px <-> pn) |
2 |
1 |
sbe |
[n / x] px <-> pn |
3 |
|
sbeq1 |
z = n -> ([z / x] px <-> [n / x] px) |
4 |
2, 3 |
syl6bb |
z = n -> ([z / x] px <-> pn) |
5 |
|
sbeq1 |
z = w -> ([z / x] px <-> [w / x] px) |
6 |
|
anr |
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> w = 0 |
7 |
6 |
sbeq1d |
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> ([w / x] px <-> [0 / x] px) |
8 |
|
hyp h0 |
x = 0 -> (px <-> p0) |
9 |
8 |
sbe |
[0 / x] px <-> p0 |
10 |
|
hyp h1 |
G -> p0 |
11 |
9, 10 |
sylibr |
G -> [0 / x] px |
12 |
11 |
anwll |
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> [0 / x] px |
13 |
7, 12 |
mpbird |
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> [w / x] px |
14 |
|
excons |
w != 0 <-> E. a E. l w = a : l |
15 |
|
anr |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> ~w = 0 |
16 |
15 |
conv ne |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> w != 0 |
17 |
14, 16 |
sylib |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. a E. l w = a : l |
18 |
|
hyp hs |
x = a : l -> (px <-> ps) |
19 |
18 |
sbe |
[a : l / x] px <-> ps |
20 |
|
anr |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> w = a : l |
21 |
20 |
sbeq1d |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> ([w / x] px <-> [a : l / x] px) |
22 |
19, 21 |
syl6bb |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> ([w / x] px <-> ps) |
23 |
|
ltconsid2 |
l < a : l |
24 |
20 |
lteq2d |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> (l < w <-> l < a : l) |
25 |
23, 24 |
mpbiri |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> l < w |
26 |
|
anlr |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> A. z (z < w -> [z / x] px) |
27 |
|
lteq1 |
z = l -> (z < w <-> l < w) |
28 |
|
hyp hl |
x = l -> (px <-> pl) |
29 |
28 |
sbe |
[l / x] px <-> pl |
30 |
|
sbeq1 |
z = l -> ([z / x] px <-> [l / x] px) |
31 |
29, 30 |
syl6bb |
z = l -> ([z / x] px <-> pl) |
32 |
27, 31 |
imeqd |
z = l -> (z < w -> [z / x] px <-> l < w -> pl) |
33 |
32 |
eale |
A. z (z < w -> [z / x] px) -> l < w -> pl |
34 |
26, 33 |
rsyl |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> l < w -> pl |
35 |
25, 34 |
mpd |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> pl |
36 |
|
hyp h2 |
G /\ pl -> ps |
37 |
36 |
exp |
G -> pl -> ps |
38 |
37 |
anwll |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> pl -> ps |
39 |
35, 38 |
mpd |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> ps |
40 |
22, 39 |
mpbird |
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> [w / x] px |
41 |
40 |
exp |
G /\ A. z (z < w -> [z / x] px) -> w = a : l -> [w / x] px |
42 |
41 |
anwl |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> w = a : l -> [w / x] px |
43 |
42 |
eexd |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. l w = a : l -> [w / x] px |
44 |
43 |
eexd |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. a E. l w = a : l -> [w / x] px |
45 |
17, 44 |
mpd |
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> [w / x] px |
46 |
13, 45 |
casesda |
G /\ A. z (z < w -> [z / x] px) -> [w / x] px |
47 |
4, 5, 46 |
indstr |
G -> pn |