Step | Hyp | Ref
| Expression |
1 | | eleq1 2820 |
. . . . 5
⊢ (𝑖 = {∅} → (𝑖 ∈ 𝑢 ↔ {∅} ∈ 𝑢)) |
2 | 1 | anbi1d 633 |
. . . 4
⊢ (𝑖 = {∅} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
3 | 2 | rexbidv 3207 |
. . 3
⊢ (𝑖 = {∅} →
(∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 ({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
4 | | mnuprdlem2.8 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
5 | | p0ex 5252 |
. . . . 5
⊢ {∅}
∈ V |
6 | 5 | prid2 4655 |
. . . 4
⊢ {∅}
∈ {∅, {∅}} |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → {∅} ∈ {∅,
{∅}}) |
8 | 3, 4, 7 | rspcdva 3529 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝐹 ({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
9 | | simpl 486 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝜑) |
10 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹) |
11 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {∅} ∈ 𝑎) → {∅} ∈ 𝑎) |
12 | | 0nep0 5225 |
. . . . . . . . . . . . . . 15
⊢ ∅
≠ {∅} |
13 | 12 | necomi 2988 |
. . . . . . . . . . . . . 14
⊢ {∅}
≠ ∅ |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {∅} ≠
∅) |
15 | | mnuprdlem2.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝐴 = ∅) |
16 | | 0ex 5176 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ V |
17 | 16 | sneqr 4727 |
. . . . . . . . . . . . . . . 16
⊢
({∅} = {𝐴}
→ ∅ = 𝐴) |
18 | 17 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢
({∅} = {𝐴}
→ 𝐴 =
∅) |
19 | 15, 18 | nsyl 142 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ {∅} = {𝐴}) |
20 | 19 | neqned 2941 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {∅} ≠ {𝐴}) |
21 | 14, 20 | nelprd 4548 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ {∅} ∈
{∅, {𝐴}}) |
22 | 21 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {∅} ∈ 𝑎) → ¬ {∅} ∈
{∅, {𝐴}}) |
23 | 11, 22 | elnelneqd 41352 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {∅} ∈ 𝑎) → ¬ 𝑎 = {∅, {𝐴}}) |
24 | 23 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎
⊆ 𝑤)) → ¬
𝑎 = {∅, {𝐴}}) |
25 | 24 | adantrl 716 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {∅, {𝐴}}) |
26 | | elpri 4539 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
27 | | mnuprdlem2.1 |
. . . . . . . . . 10
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} |
28 | 26, 27 | eleq2s 2851 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
29 | 28 | ord 863 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {∅, {𝐴}} → 𝑎 = {{∅}, {𝐵}})) |
30 | 10, 25, 29 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {{∅}, {𝐵}}) |
31 | 30 | unieqd 4811 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪
{{∅}, {𝐵}}) |
32 | | snex 5299 |
. . . . . . . 8
⊢ {𝐵} ∈ V |
33 | 5, 32 | unipr 4815 |
. . . . . . 7
⊢ ∪ {{∅}, {𝐵}} = ({∅} ∪ {𝐵}) |
34 | | df-pr 4520 |
. . . . . . 7
⊢ {∅,
𝐵} = ({∅} ∪
{𝐵}) |
35 | 33, 34 | eqtr4i 2764 |
. . . . . 6
⊢ ∪ {{∅}, {𝐵}} = {∅, 𝐵} |
36 | 31, 35 | eqtrdi 2789 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {∅, 𝐵}) |
37 | | simprrr 782 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤) |
38 | 36, 37 | eqsstrrd 3917 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {∅, 𝐵} ⊆ 𝑤) |
39 | | mnuprdlem2.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
40 | | prssg 4708 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐵 ∈
𝑈) → ((∅ ∈
𝑤 ∧ 𝐵 ∈ 𝑤) ↔ {∅, 𝐵} ⊆ 𝑤)) |
41 | 16, 39, 40 | sylancr 590 |
. . . . 5
⊢ (𝜑 → ((∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤) ↔ {∅, 𝐵} ⊆ 𝑤)) |
42 | 41 | biimprd 251 |
. . . 4
⊢ (𝜑 → ({∅, 𝐵} ⊆ 𝑤 → (∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))) |
43 | 9, 38, 42 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → (∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)) |
44 | 43 | simprd 499 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐵 ∈ 𝑤) |
45 | | eleq2w 2816 |
. . 3
⊢ (𝑢 = 𝑎 → ({∅} ∈ 𝑢 ↔ {∅} ∈ 𝑎)) |
46 | | unieq 4808 |
. . . 4
⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪
𝑎) |
47 | 46 | sseq1d 3909 |
. . 3
⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤)) |
48 | 45, 47 | anbi12d 634 |
. 2
⊢ (𝑢 = 𝑎 → (({∅} ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ({∅} ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) |
49 | 8, 44, 48 | rexlimddvcbvw 41356 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑤) |