Step | Hyp | Ref
| Expression |
1 | | inss2 3476 |
. . 3
⊢ (A ∩ Nn ) ⊆ Nn |
2 | | inss1 3475 |
. . . . 5
⊢ (A ∩ Nn ) ⊆ A |
3 | 2 | sseli 3269 |
. . . 4
⊢
(0c ∈ (A ∩ Nn ) →
0c ∈ A) |
4 | 3 | con3i 127 |
. . 3
⊢ (¬
0c ∈ A → ¬ 0c ∈ (A ∩
Nn )) |
5 | | phiall.1 |
. . . . 5
⊢ A ∈
V |
6 | | nncex 4396 |
. . . . 5
⊢ Nn ∈
V |
7 | 5, 6 | inex 4105 |
. . . 4
⊢ (A ∩ Nn ) ∈ V |
8 | 7 | phialllem1 4616 |
. . 3
⊢ (((A ∩ Nn ) ⊆ Nn ∧ ¬ 0c ∈ (A ∩
Nn )) → ∃y(A ∩ Nn ) = Phi y) |
9 | 1, 4, 8 | sylancr 644 |
. 2
⊢ (¬
0c ∈ A → ∃y(A ∩ Nn ) = Phi y) |
10 | | uncom 3408 |
. . . . . . 7
⊢ ((A ∖ Nn ) ∪ (A ∩
Nn )) = ((A
∩ Nn ) ∪ (A ∖ Nn )) |
11 | | inundif 3628 |
. . . . . . 7
⊢ ((A ∩ Nn ) ∪
(A ∖
Nn )) = A |
12 | 10, 11 | eqtri 2373 |
. . . . . 6
⊢ ((A ∖ Nn ) ∪ (A ∩
Nn )) = A |
13 | | uneq2 3412 |
. . . . . 6
⊢ ((A ∩ Nn ) = Phi y →
((A ∖
Nn ) ∪ (A
∩ Nn )) = ((A ∖ Nn ) ∪ Phi y)) |
14 | 12, 13 | syl5eqr 2399 |
. . . . 5
⊢ ((A ∩ Nn ) = Phi y →
A = ((A
∖ Nn ) ∪
Phi y)) |
15 | | phiun 4614 |
. . . . . 6
⊢ Phi ((A ∖ Nn ) ∪ y) = ( Phi (A ∖ Nn ) ∪ Phi y) |
16 | | incom 3448 |
. . . . . . . . 9
⊢ ((A ∖ Nn ) ∩ Nn ) = ( Nn ∩ (A ∖ Nn
)) |
17 | | disjdif 3622 |
. . . . . . . . 9
⊢ ( Nn ∩ (A ∖ Nn )) = ∅ |
18 | 16, 17 | eqtri 2373 |
. . . . . . . 8
⊢ ((A ∖ Nn ) ∩ Nn ) = ∅ |
19 | | phidisjnn 4615 |
. . . . . . . 8
⊢ (((A ∖ Nn ) ∩ Nn ) = ∅ → Phi
(A ∖ Nn ) = (A ∖ Nn )) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ Phi (A ∖ Nn ) = (A ∖ Nn ) |
21 | 20 | uneq1i 3414 |
. . . . . 6
⊢ ( Phi (A ∖ Nn ) ∪ Phi y) = ((A ∖ Nn ) ∪ Phi y) |
22 | 15, 21 | eqtri 2373 |
. . . . 5
⊢ Phi ((A ∖ Nn ) ∪ y) = ((A ∖ Nn ) ∪ Phi y) |
23 | 14, 22 | syl6eqr 2403 |
. . . 4
⊢ ((A ∩ Nn ) = Phi y →
A = Phi
((A ∖ Nn ) ∪ y)) |
24 | 5, 6 | difex 4107 |
. . . . . 6
⊢ (A ∖ Nn ) ∈
V |
25 | | vex 2862 |
. . . . . 6
⊢ y ∈
V |
26 | 24, 25 | unex 4106 |
. . . . 5
⊢ ((A ∖ Nn ) ∪ y) ∈ V |
27 | | phieq 4570 |
. . . . . 6
⊢ (x = ((A ∖ Nn ) ∪ y) → Phi x = Phi ((A ∖ Nn ) ∪ y)) |
28 | 27 | eqeq2d 2364 |
. . . . 5
⊢ (x = ((A ∖ Nn ) ∪ y) → (A =
Phi x ↔
A = Phi
((A ∖ Nn ) ∪ y))) |
29 | 26, 28 | spcev 2946 |
. . . 4
⊢ (A = Phi ((A ∖ Nn ) ∪ y) →
∃x
A = Phi
x) |
30 | 23, 29 | syl 15 |
. . 3
⊢ ((A ∩ Nn ) = Phi y → ∃x A = Phi x) |
31 | 30 | exlimiv 1634 |
. 2
⊢ (∃y(A ∩ Nn ) = Phi y → ∃x A = Phi x) |
32 | 9, 31 | syl 15 |
1
⊢ (¬
0c ∈ A → ∃x A = Phi x) |