| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. . . . 5
⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢)) |
| 2 | 1 | anbi1d 631 |
. . . 4
⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
| 3 | 2 | rexbidv 3179 |
. . 3
⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
| 4 | | mnuprdlem1.8 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
| 5 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 6 | 5 | prid1 4762 |
. . . 4
⊢ ∅
∈ {∅, {∅}} |
| 7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → ∅ ∈ {∅,
{∅}}) |
| 8 | 3, 4, 7 | rspcdva 3623 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
| 9 | | mnuprdlem1.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| 10 | 9 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈) |
| 11 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹) |
| 12 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎) |
| 13 | | 0nep0 5358 |
. . . . . . . . . . . . 13
⊢ ∅
≠ {∅} |
| 14 | 13 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ≠
{∅}) |
| 15 | | mnuprdlem1.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
| 16 | 15 | snn0d 4775 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐵} ≠ ∅) |
| 17 | 16 | necomd 2996 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ≠ {𝐵}) |
| 18 | 14, 17 | nelprd 4657 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∅ ∈
{{∅}, {𝐵}}) |
| 19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈
{{∅}, {𝐵}}) |
| 20 | 12, 19 | elnelneqd 44215 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}}) |
| 21 | 20 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎
⊆ 𝑤)) → ¬
𝑎 = {{∅}, {𝐵}}) |
| 22 | 21 | adantrl 716 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}}) |
| 23 | | elpri 4649 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
| 24 | | mnuprdlem1.1 |
. . . . . . . . . 10
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} |
| 25 | 23, 24 | eleq2s 2859 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
| 26 | 25 | orcomd 872 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}})) |
| 27 | 26 | ord 865 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}})) |
| 28 | 11, 22, 27 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}}) |
| 29 | 28 | unieqd 4920 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪
{∅, {𝐴}}) |
| 30 | | snex 5436 |
. . . . . . 7
⊢ {𝐴} ∈ V |
| 31 | 5, 30 | unipr 4924 |
. . . . . 6
⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴}) |
| 32 | | uncom 4158 |
. . . . . 6
⊢ (∅
∪ {𝐴}) = ({𝐴} ∪
∅) |
| 33 | | un0 4394 |
. . . . . 6
⊢ ({𝐴} ∪ ∅) = {𝐴} |
| 34 | 31, 32, 33 | 3eqtri 2769 |
. . . . 5
⊢ ∪ {∅, {𝐴}} = {𝐴} |
| 35 | 29, 34 | eqtrdi 2793 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴}) |
| 36 | | simprrr 782 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤) |
| 37 | 35, 36 | eqsstrrd 4019 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤) |
| 38 | | snssg 4783 |
. . . 4
⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤)) |
| 39 | 38 | biimprd 248 |
. . 3
⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤)) |
| 40 | 10, 37, 39 | sylc 65 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤) |
| 41 | | eleq2w 2825 |
. . 3
⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎)) |
| 42 | | unieq 4918 |
. . . 4
⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪
𝑎) |
| 43 | 42 | sseq1d 4015 |
. . 3
⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤)) |
| 44 | 41, 43 | anbi12d 632 |
. 2
⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) |
| 45 | 8, 40, 44 | rexlimddvcbvw 44219 |
1
⊢ (𝜑 → 𝐴 ∈ 𝑤) |