Step |
Hyp |
Ref |
Expression |
1 |
|
mnuprdlem1.1 |
⊢ 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } } |
2 |
|
mnuprdlem1.3 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
3 |
|
mnuprdlem1.4 |
⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |
4 |
|
mnuprdlem1.8 |
⊢ ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) |
5 |
|
eleq1 |
⊢ ( 𝑖 = ∅ → ( 𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢 ) ) |
6 |
5
|
anbi1d |
⊢ ( 𝑖 = ∅ → ( ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( ∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑖 = ∅ → ( ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝐹 ( ∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) |
8 |
|
0ex |
⊢ ∅ ∈ V |
9 |
8
|
prid1 |
⊢ ∅ ∈ { ∅ , { ∅ } } |
10 |
9
|
a1i |
⊢ ( 𝜑 → ∅ ∈ { ∅ , { ∅ } } ) |
11 |
7 4 10
|
rspcdva |
⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐹 ( ∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) |
12 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝐴 ∈ 𝑈 ) |
13 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝑎 ∈ 𝐹 ) |
14 |
|
simpr |
⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑎 ) → ∅ ∈ 𝑎 ) |
15 |
|
0nep0 |
⊢ ∅ ≠ { ∅ } |
16 |
15
|
a1i |
⊢ ( 𝜑 → ∅ ≠ { ∅ } ) |
17 |
3
|
snn0d |
⊢ ( 𝜑 → { 𝐵 } ≠ ∅ ) |
18 |
17
|
necomd |
⊢ ( 𝜑 → ∅ ≠ { 𝐵 } ) |
19 |
16 18
|
nelprd |
⊢ ( 𝜑 → ¬ ∅ ∈ { { ∅ } , { 𝐵 } } ) |
20 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑎 ) → ¬ ∅ ∈ { { ∅ } , { 𝐵 } } ) |
21 |
14 20
|
elnelneqd |
⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑎 ) → ¬ 𝑎 = { { ∅ } , { 𝐵 } } ) |
22 |
21
|
adantrr |
⊢ ( ( 𝜑 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) → ¬ 𝑎 = { { ∅ } , { 𝐵 } } ) |
23 |
22
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ¬ 𝑎 = { { ∅ } , { 𝐵 } } ) |
24 |
|
elpri |
⊢ ( 𝑎 ∈ { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } } → ( 𝑎 = { ∅ , { 𝐴 } } ∨ 𝑎 = { { ∅ } , { 𝐵 } } ) ) |
25 |
24 1
|
eleq2s |
⊢ ( 𝑎 ∈ 𝐹 → ( 𝑎 = { ∅ , { 𝐴 } } ∨ 𝑎 = { { ∅ } , { 𝐵 } } ) ) |
26 |
25
|
orcomd |
⊢ ( 𝑎 ∈ 𝐹 → ( 𝑎 = { { ∅ } , { 𝐵 } } ∨ 𝑎 = { ∅ , { 𝐴 } } ) ) |
27 |
26
|
ord |
⊢ ( 𝑎 ∈ 𝐹 → ( ¬ 𝑎 = { { ∅ } , { 𝐵 } } → 𝑎 = { ∅ , { 𝐴 } } ) ) |
28 |
13 23 27
|
sylc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝑎 = { ∅ , { 𝐴 } } ) |
29 |
28
|
unieqd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ∪ 𝑎 = ∪ { ∅ , { 𝐴 } } ) |
30 |
|
snex |
⊢ { 𝐴 } ∈ V |
31 |
8 30
|
unipr |
⊢ ∪ { ∅ , { 𝐴 } } = ( ∅ ∪ { 𝐴 } ) |
32 |
|
uncom |
⊢ ( ∅ ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ∅ ) |
33 |
|
un0 |
⊢ ( { 𝐴 } ∪ ∅ ) = { 𝐴 } |
34 |
31 32 33
|
3eqtri |
⊢ ∪ { ∅ , { 𝐴 } } = { 𝐴 } |
35 |
29 34
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ∪ 𝑎 = { 𝐴 } ) |
36 |
|
simprrr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ∪ 𝑎 ⊆ 𝑤 ) |
37 |
35 36
|
eqsstrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → { 𝐴 } ⊆ 𝑤 ) |
38 |
|
snssg |
⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ∈ 𝑤 ↔ { 𝐴 } ⊆ 𝑤 ) ) |
39 |
38
|
biimprd |
⊢ ( 𝐴 ∈ 𝑈 → ( { 𝐴 } ⊆ 𝑤 → 𝐴 ∈ 𝑤 ) ) |
40 |
12 37 39
|
sylc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝐴 ∈ 𝑤 ) |
41 |
|
eleq2w |
⊢ ( 𝑢 = 𝑎 → ( ∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎 ) ) |
42 |
|
unieq |
⊢ ( 𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎 ) |
43 |
42
|
sseq1d |
⊢ ( 𝑢 = 𝑎 → ( ∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤 ) ) |
44 |
41 43
|
anbi12d |
⊢ ( 𝑢 = 𝑎 → ( ( ∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( ∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) |
45 |
11 40 44
|
rexlimddvcbvw |
⊢ ( 𝜑 → 𝐴 ∈ 𝑤 ) |