| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ineq2 |
⊢ ( 𝑦 = 𝑣 → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑣 ) ) |
| 2 |
1
|
eleq2d |
⊢ ( 𝑦 = 𝑣 → ( 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ) |
| 3 |
2
|
eubidv |
⊢ ( 𝑦 = 𝑣 → ( ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ) |
| 4 |
3
|
imbi2d |
⊢ ( 𝑦 = 𝑣 → ( ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ) ) |
| 5 |
4
|
ralbidv |
⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ) ) |
| 6 |
5
|
cbvexvw |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑣 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ) |
| 7 |
|
indi |
⊢ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) = ( ( 𝑧 ∩ 𝑣 ) ∪ ( 𝑧 ∩ { 𝑢 } ) ) |
| 8 |
|
elssuni |
⊢ ( 𝑧 ∈ 𝑥 → 𝑧 ⊆ ∪ 𝑥 ) |
| 9 |
8
|
ssneld |
⊢ ( 𝑧 ∈ 𝑥 → ( ¬ 𝑢 ∈ ∪ 𝑥 → ¬ 𝑢 ∈ 𝑧 ) ) |
| 10 |
|
disjsn |
⊢ ( ( 𝑧 ∩ { 𝑢 } ) = ∅ ↔ ¬ 𝑢 ∈ 𝑧 ) |
| 11 |
9 10
|
imbitrrdi |
⊢ ( 𝑧 ∈ 𝑥 → ( ¬ 𝑢 ∈ ∪ 𝑥 → ( 𝑧 ∩ { 𝑢 } ) = ∅ ) ) |
| 12 |
11
|
impcom |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑧 ∩ { 𝑢 } ) = ∅ ) |
| 13 |
12
|
uneq2d |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( ( 𝑧 ∩ 𝑣 ) ∪ ( 𝑧 ∩ { 𝑢 } ) ) = ( ( 𝑧 ∩ 𝑣 ) ∪ ∅ ) ) |
| 14 |
|
un0 |
⊢ ( ( 𝑧 ∩ 𝑣 ) ∪ ∅ ) = ( 𝑧 ∩ 𝑣 ) |
| 15 |
13 14
|
eqtrdi |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( ( 𝑧 ∩ 𝑣 ) ∪ ( 𝑧 ∩ { 𝑢 } ) ) = ( 𝑧 ∩ 𝑣 ) ) |
| 16 |
7 15
|
eqtr2id |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑧 ∩ 𝑣 ) = ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) |
| 17 |
16
|
eleq2d |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ↔ 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) |
| 18 |
17
|
eubidv |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ↔ ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) |
| 19 |
18
|
imbi2d |
⊢ ( ( ¬ 𝑢 ∈ ∪ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ↔ ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) |
| 20 |
19
|
ralbidva |
⊢ ( ¬ 𝑢 ∈ ∪ 𝑥 → ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) |
| 21 |
|
vsnid |
⊢ 𝑢 ∈ { 𝑢 } |
| 22 |
21
|
olci |
⊢ ( 𝑢 ∈ 𝑣 ∨ 𝑢 ∈ { 𝑢 } ) |
| 23 |
|
elun |
⊢ ( 𝑢 ∈ ( 𝑣 ∪ { 𝑢 } ) ↔ ( 𝑢 ∈ 𝑣 ∨ 𝑢 ∈ { 𝑢 } ) ) |
| 24 |
22 23
|
mpbir |
⊢ 𝑢 ∈ ( 𝑣 ∪ { 𝑢 } ) |
| 25 |
|
elssuni |
⊢ ( ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 → ( 𝑣 ∪ { 𝑢 } ) ⊆ ∪ 𝑥 ) |
| 26 |
25
|
sseld |
⊢ ( ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 → ( 𝑢 ∈ ( 𝑣 ∪ { 𝑢 } ) → 𝑢 ∈ ∪ 𝑥 ) ) |
| 27 |
24 26
|
mpi |
⊢ ( ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 → 𝑢 ∈ ∪ 𝑥 ) |
| 28 |
27
|
con3i |
⊢ ( ¬ 𝑢 ∈ ∪ 𝑥 → ¬ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ) |
| 29 |
28
|
biantrurd |
⊢ ( ¬ 𝑢 ∈ ∪ 𝑥 → ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ↔ ( ¬ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) ) |
| 30 |
20 29
|
bitrd |
⊢ ( ¬ 𝑢 ∈ ∪ 𝑥 → ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) ↔ ( ¬ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) ) |
| 31 |
|
vex |
⊢ 𝑣 ∈ V |
| 32 |
|
vsnex |
⊢ { 𝑢 } ∈ V |
| 33 |
31 32
|
unex |
⊢ ( 𝑣 ∪ { 𝑢 } ) ∈ V |
| 34 |
|
eleq1 |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( 𝑦 ∈ 𝑥 ↔ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ) ) |
| 35 |
34
|
notbid |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( ¬ 𝑦 ∈ 𝑥 ↔ ¬ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ) ) |
| 36 |
|
ineq2 |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) |
| 37 |
36
|
eleq2d |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) |
| 38 |
37
|
eubidv |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) |
| 39 |
38
|
imbi2d |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) |
| 40 |
39
|
ralbidv |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) |
| 41 |
35 40
|
anbi12d |
⊢ ( 𝑦 = ( 𝑣 ∪ { 𝑢 } ) → ( ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ¬ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) ) ) |
| 42 |
33 41
|
spcev |
⊢ ( ( ¬ ( 𝑣 ∪ { 𝑢 } ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ ( 𝑣 ∪ { 𝑢 } ) ) ) ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) |
| 43 |
30 42
|
biimtrdi |
⊢ ( ¬ 𝑢 ∈ ∪ 𝑥 → ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) ) |
| 44 |
|
vuniex |
⊢ ∪ 𝑥 ∈ V |
| 45 |
|
eleq2 |
⊢ ( 𝑦 = ∪ 𝑥 → ( 𝑢 ∈ 𝑦 ↔ 𝑢 ∈ ∪ 𝑥 ) ) |
| 46 |
45
|
notbid |
⊢ ( 𝑦 = ∪ 𝑥 → ( ¬ 𝑢 ∈ 𝑦 ↔ ¬ 𝑢 ∈ ∪ 𝑥 ) ) |
| 47 |
46
|
exbidv |
⊢ ( 𝑦 = ∪ 𝑥 → ( ∃ 𝑢 ¬ 𝑢 ∈ 𝑦 ↔ ∃ 𝑢 ¬ 𝑢 ∈ ∪ 𝑥 ) ) |
| 48 |
|
nalset |
⊢ ¬ ∃ 𝑦 ∀ 𝑢 𝑢 ∈ 𝑦 |
| 49 |
|
alexn |
⊢ ( ∀ 𝑦 ∃ 𝑢 ¬ 𝑢 ∈ 𝑦 ↔ ¬ ∃ 𝑦 ∀ 𝑢 𝑢 ∈ 𝑦 ) |
| 50 |
48 49
|
mpbir |
⊢ ∀ 𝑦 ∃ 𝑢 ¬ 𝑢 ∈ 𝑦 |
| 51 |
50
|
spi |
⊢ ∃ 𝑢 ¬ 𝑢 ∈ 𝑦 |
| 52 |
44 47 51
|
vtocl |
⊢ ∃ 𝑢 ¬ 𝑢 ∈ ∪ 𝑥 |
| 53 |
43 52
|
exlimiiv |
⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) |
| 54 |
53
|
exlimiv |
⊢ ( ∃ 𝑣 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑣 ) ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) |
| 55 |
6 54
|
sylbi |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) |
| 56 |
|
exsimpr |
⊢ ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) |
| 57 |
55 56
|
impbii |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) |