Step | Hyp | Ref | Expression |
1 |
|
elres |
p e. (\ x, a) |` A <-> p e. \ x, a /\ fst p e. A |
2 |
|
elres |
p e. (\ x, b) |` A <-> p e. \ x, b /\ fst p e. A |
3 |
|
aneq1a |
(fst p e. A -> (p e. \ x, a <-> p e. \ x, b)) -> (p e. \ x, a /\ fst p e. A <-> p e. \ x, b /\ fst p e. A) |
4 |
|
ellam |
p e. \ x, a <-> E. x p = x, a |
5 |
|
ellam |
p e. \ x, b <-> E. x p = x, b |
6 |
|
exeq |
A. x (p = x, a <-> p = x, b) -> (E. x p = x, a <-> E. x p = x, b) |
7 |
|
fstpr |
fst (x, a) = x |
8 |
|
anr |
fst p e. A /\ (x e. A -> a = b) /\ p = x, a -> p = x, a |
9 |
8 |
fsteqd |
fst p e. A /\ (x e. A -> a = b) /\ p = x, a -> fst p = fst (x, a) |
10 |
7, 9 |
syl6eq |
fst p e. A /\ (x e. A -> a = b) /\ p = x, a -> fst p = x |
11 |
|
fstpr |
fst (x, b) = x |
12 |
|
anr |
fst p e. A /\ (x e. A -> a = b) /\ p = x, b -> p = x, b |
13 |
12 |
fsteqd |
fst p e. A /\ (x e. A -> a = b) /\ p = x, b -> fst p = fst (x, b) |
14 |
11, 13 |
syl6eq |
fst p e. A /\ (x e. A -> a = b) /\ p = x, b -> fst p = x |
15 |
|
anr |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> fst p = x |
16 |
15 |
eleq1d |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> (fst p e. A <-> x e. A) |
17 |
|
anll |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> fst p e. A |
18 |
16, 17 |
mpbid |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> x e. A |
19 |
|
anlr |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> x e. A -> a = b |
20 |
18, 19 |
mpd |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> a = b |
21 |
20 |
preq2d |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> x, a = x, b |
22 |
21 |
eqeq2d |
fst p e. A /\ (x e. A -> a = b) /\ fst p = x -> (p = x, a <-> p = x, b) |
23 |
10, 14, 22 |
rbida |
fst p e. A /\ (x e. A -> a = b) -> (p = x, a <-> p = x, b) |
24 |
23 |
exp |
fst p e. A -> (x e. A -> a = b) -> (p = x, a <-> p = x, b) |
25 |
24 |
alimd |
fst p e. A -> A. x (x e. A -> a = b) -> A. x (p = x, a <-> p = x, b) |
26 |
25 |
impcom |
A. x (x e. A -> a = b) /\ fst p e. A -> A. x (p = x, a <-> p = x, b) |
27 |
6, 26 |
syl |
A. x (x e. A -> a = b) /\ fst p e. A -> (E. x p = x, a <-> E. x p = x, b) |
28 |
4, 5, 27 |
bitr4g |
A. x (x e. A -> a = b) /\ fst p e. A -> (p e. \ x, a <-> p e. \ x, b) |
29 |
3, 28 |
syla |
A. x (x e. A -> a = b) -> (p e. \ x, a /\ fst p e. A <-> p e. \ x, b /\ fst p e. A) |
30 |
1, 2, 29 |
bitr4g |
A. x (x e. A -> a = b) -> (p e. (\ x, a) |` A <-> p e. (\ x, b) |` A) |
31 |
30 |
eqrd |
A. x (x e. A -> a = b) -> (\ x, a) |` A == (\ x, b) |` A |