Step | Hyp | Ref
| Expression |
1 | | df-op 4566 |
. . . . 5
⊢ 〈A, B〉 = ({x ∣ ∃y ∈ A x = Phi y} ∪ {x
∣ ∃y ∈ B x = ( Phi y ∪ {0c})}) |
2 | 1 | eleq2i 2417 |
. . . 4
⊢ ( Phi z ∈ 〈A, B〉 ↔ Phi z ∈ ({x ∣ ∃y ∈ A x = Phi y} ∪ {x
∣ ∃y ∈ B x = ( Phi y ∪ {0c})})) |
3 | | elun 3220 |
. . . 4
⊢ ( Phi z ∈ ({x ∣ ∃y ∈ A x = Phi y} ∪
{x ∣
∃y ∈ B x = ( Phi y ∪ {0c})}) ↔ ( Phi z ∈ {x ∣ ∃y ∈ A x = Phi y} ∨ Phi z ∈ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})})) |
4 | | vex 2862 |
. . . . . . 7
⊢ z ∈
V |
5 | 4 | phiex 4572 |
. . . . . 6
⊢ Phi z ∈ V |
6 | | eqeq1 2359 |
. . . . . . . . 9
⊢ (x = Phi z → (x =
Phi y ↔
Phi z = Phi y)) |
7 | | phi11 4596 |
. . . . . . . . . 10
⊢ (z = y ↔
Phi z = Phi y) |
8 | | equcom 1680 |
. . . . . . . . . 10
⊢ (z = y ↔
y = z) |
9 | 7, 8 | bitr3i 242 |
. . . . . . . . 9
⊢ ( Phi z = Phi y ↔
y = z) |
10 | 6, 9 | syl6bb 252 |
. . . . . . . 8
⊢ (x = Phi z → (x =
Phi y ↔
y = z)) |
11 | 10 | rexbidv 2635 |
. . . . . . 7
⊢ (x = Phi z → (∃y ∈ A x = Phi y ↔ ∃y ∈ A y = z)) |
12 | | risset 2661 |
. . . . . . 7
⊢ (z ∈ A ↔ ∃y ∈ A y = z) |
13 | 11, 12 | syl6bbr 254 |
. . . . . 6
⊢ (x = Phi z → (∃y ∈ A x = Phi y ↔ z ∈ A)) |
14 | 5, 13 | elab 2985 |
. . . . 5
⊢ ( Phi z ∈ {x ∣ ∃y ∈ A x = Phi y} ↔
z ∈
A) |
15 | | eqeq1 2359 |
. . . . . . 7
⊢ (x = Phi z → (x =
( Phi y ∪
{0c}) ↔ Phi z = ( Phi y ∪ {0c}))) |
16 | 15 | rexbidv 2635 |
. . . . . 6
⊢ (x = Phi z → (∃y ∈ B x = ( Phi y ∪ {0c}) ↔ ∃y ∈ B Phi z = ( Phi y ∪
{0c}))) |
17 | 5, 16 | elab 2985 |
. . . . 5
⊢ ( Phi z ∈ {x ∣ ∃y ∈ B x = ( Phi y ∪
{0c})} ↔ ∃y ∈ B Phi z = ( Phi y ∪ {0c})) |
18 | 14, 17 | orbi12i 507 |
. . . 4
⊢ (( Phi z ∈ {x ∣ ∃y ∈ A x = Phi y} ∨ Phi z ∈ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})}) ↔ (z ∈ A ∨ ∃y ∈ B Phi z = ( Phi y ∪
{0c}))) |
19 | 2, 3, 18 | 3bitri 262 |
. . 3
⊢ ( Phi z ∈ 〈A, B〉 ↔ (z
∈ A ∨ ∃y ∈ B Phi z = ( Phi y ∪ {0c}))) |
20 | | phieq 4570 |
. . . . 5
⊢ (x = z →
Phi x = Phi z) |
21 | 20 | eleq1d 2419 |
. . . 4
⊢ (x = z →
( Phi x ∈ 〈A, B〉 ↔ Phi z ∈ 〈A, B〉)) |
22 | | df-proj1 4567 |
. . . 4
⊢ Proj1 〈A, B〉 = {x ∣ Phi x ∈ 〈A, B〉} |
23 | 4, 21, 22 | elab2 2988 |
. . 3
⊢ (z ∈ Proj1 〈A, B〉 ↔ Phi z ∈ 〈A, B〉) |
24 | | 0cnelphi 4597 |
. . . . . . 7
⊢ ¬
0c ∈
Phi z |
25 | | ssun2 3427 |
. . . . . . . . 9
⊢
{0c} ⊆ ( Phi y ∪
{0c}) |
26 | | 0cex 4392 |
. . . . . . . . . 10
⊢
0c ∈
V |
27 | 26 | snid 3760 |
. . . . . . . . 9
⊢
0c ∈
{0c} |
28 | 25, 27 | sselii 3270 |
. . . . . . . 8
⊢
0c ∈ ( Phi y ∪
{0c}) |
29 | | eleq2 2414 |
. . . . . . . 8
⊢ ( Phi z = ( Phi y ∪
{0c}) → (0c ∈ Phi z ↔ 0c ∈ ( Phi y ∪ {0c}))) |
30 | 28, 29 | mpbiri 224 |
. . . . . . 7
⊢ ( Phi z = ( Phi y ∪
{0c}) → 0c ∈ Phi z) |
31 | 24, 30 | mto 167 |
. . . . . 6
⊢ ¬ Phi z = ( Phi y ∪
{0c}) |
32 | 31 | a1i 10 |
. . . . 5
⊢ (y ∈ B → ¬ Phi
z = ( Phi
y ∪
{0c})) |
33 | 32 | nrex 2716 |
. . . 4
⊢ ¬ ∃y ∈ B Phi z = ( Phi y ∪
{0c}) |
34 | 33 | biorfi 396 |
. . 3
⊢ (z ∈ A ↔ (z
∈ A ∨ ∃y ∈ B Phi z = ( Phi y ∪ {0c}))) |
35 | 19, 23, 34 | 3bitr4i 268 |
. 2
⊢ (z ∈ Proj1 〈A, B〉 ↔ z
∈ A) |
36 | 35 | eqriv 2350 |
1
⊢ Proj1 〈A, B〉 = A |