Step | Hyp | Ref
| Expression |
1 | | eleq1 2826 |
. . . . 5
⊢ (𝑖 = {∅} → (𝑖 ∈ 𝑢 ↔ {∅} ∈ 𝑢)) |
2 | 1 | anbi1d 630 |
. . . 4
⊢ (𝑖 = {∅} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
3 | 2 | rexbidv 3226 |
. . 3
⊢ (𝑖 = {∅} →
(∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 ({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
4 | | mnuprdlem2.8 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
5 | | p0ex 5307 |
. . . . 5
⊢ {∅}
∈ V |
6 | 5 | prid2 4699 |
. . . 4
⊢ {∅}
∈ {∅, {∅}} |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → {∅} ∈ {∅,
{∅}}) |
8 | 3, 4, 7 | rspcdva 3562 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝐹 ({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
9 | | simpl 483 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝜑) |
10 | | simprl 768 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹) |
11 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {∅} ∈ 𝑎) → {∅} ∈ 𝑎) |
12 | | 0nep0 5280 |
. . . . . . . . . . . . . . 15
⊢ ∅
≠ {∅} |
13 | 12 | necomi 2998 |
. . . . . . . . . . . . . 14
⊢ {∅}
≠ ∅ |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {∅} ≠
∅) |
15 | | mnuprdlem2.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝐴 = ∅) |
16 | | 0ex 5231 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ V |
17 | 16 | sneqr 4771 |
. . . . . . . . . . . . . . . 16
⊢
({∅} = {𝐴}
→ ∅ = 𝐴) |
18 | 17 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢
({∅} = {𝐴}
→ 𝐴 =
∅) |
19 | 15, 18 | nsyl 140 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ {∅} = {𝐴}) |
20 | 19 | neqned 2950 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {∅} ≠ {𝐴}) |
21 | 14, 20 | nelprd 4592 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ {∅} ∈
{∅, {𝐴}}) |
22 | 21 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {∅} ∈ 𝑎) → ¬ {∅} ∈
{∅, {𝐴}}) |
23 | 11, 22 | elnelneqd 41813 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {∅} ∈ 𝑎) → ¬ 𝑎 = {∅, {𝐴}}) |
24 | 23 | adantrr 714 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎
⊆ 𝑤)) → ¬
𝑎 = {∅, {𝐴}}) |
25 | 24 | adantrl 713 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {∅, {𝐴}}) |
26 | | elpri 4583 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
27 | | mnuprdlem2.1 |
. . . . . . . . . 10
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} |
28 | 26, 27 | eleq2s 2857 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
29 | 28 | ord 861 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {∅, {𝐴}} → 𝑎 = {{∅}, {𝐵}})) |
30 | 10, 25, 29 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {{∅}, {𝐵}}) |
31 | 30 | unieqd 4853 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪
{{∅}, {𝐵}}) |
32 | | snex 5354 |
. . . . . . . 8
⊢ {𝐵} ∈ V |
33 | 5, 32 | unipr 4857 |
. . . . . . 7
⊢ ∪ {{∅}, {𝐵}} = ({∅} ∪ {𝐵}) |
34 | | df-pr 4564 |
. . . . . . 7
⊢ {∅,
𝐵} = ({∅} ∪
{𝐵}) |
35 | 33, 34 | eqtr4i 2769 |
. . . . . 6
⊢ ∪ {{∅}, {𝐵}} = {∅, 𝐵} |
36 | 31, 35 | eqtrdi 2794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {∅, 𝐵}) |
37 | | simprrr 779 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤) |
38 | 36, 37 | eqsstrrd 3960 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {∅, 𝐵} ⊆ 𝑤) |
39 | | mnuprdlem2.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
40 | | prssg 4752 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐵 ∈
𝑈) → ((∅ ∈
𝑤 ∧ 𝐵 ∈ 𝑤) ↔ {∅, 𝐵} ⊆ 𝑤)) |
41 | 16, 39, 40 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ((∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤) ↔ {∅, 𝐵} ⊆ 𝑤)) |
42 | 41 | biimprd 247 |
. . . 4
⊢ (𝜑 → ({∅, 𝐵} ⊆ 𝑤 → (∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))) |
43 | 9, 38, 42 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → (∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)) |
44 | 43 | simprd 496 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐵 ∈ 𝑤) |
45 | | eleq2w 2822 |
. . 3
⊢ (𝑢 = 𝑎 → ({∅} ∈ 𝑢 ↔ {∅} ∈ 𝑎)) |
46 | | unieq 4850 |
. . . 4
⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪
𝑎) |
47 | 46 | sseq1d 3952 |
. . 3
⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤)) |
48 | 45, 47 | anbi12d 631 |
. 2
⊢ (𝑢 = 𝑎 → (({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) |
49 | 8, 44, 48 | rexlimddvcbvw 41817 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑤) |