Step | Hyp | Ref
| Expression |
1 | | eleq1 2900 |
. . . . 5
⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢)) |
2 | 1 | anbi1d 631 |
. . . 4
⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
3 | 2 | rexbidv 3297 |
. . 3
⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
4 | | mnuprdlem1.8 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
5 | | 0ex 5211 |
. . . . 5
⊢ ∅
∈ V |
6 | 5 | prid1 4698 |
. . . 4
⊢ ∅
∈ {∅, {∅}} |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → ∅ ∈ {∅,
{∅}}) |
8 | 3, 4, 7 | rspcdva 3625 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
9 | | mnuprdlem1.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
10 | 9 | adantr 483 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈) |
11 | | simprl 769 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹) |
12 | | simpr 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎) |
13 | | 0nep0 5258 |
. . . . . . . . . . . . 13
⊢ ∅
≠ {∅} |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ≠
{∅}) |
15 | | mnuprdlem1.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
16 | | snnzg 4710 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑈 → {𝐵} ≠ ∅) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐵} ≠ ∅) |
18 | 17 | necomd 3071 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ≠ {𝐵}) |
19 | 14, 18 | nelprd 4596 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∅ ∈
{{∅}, {𝐵}}) |
20 | 19 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈
{{∅}, {𝐵}}) |
21 | 12, 20 | elnelneqd 40604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}}) |
22 | 21 | adantrr 715 |
. . . . . . . 8
⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎
⊆ 𝑤)) → ¬
𝑎 = {{∅}, {𝐵}}) |
23 | 22 | adantrl 714 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}}) |
24 | | elpri 4589 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
25 | | mnuprdlem1.1 |
. . . . . . . . . 10
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} |
26 | 24, 25 | eleq2s 2931 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}})) |
27 | 26 | orcomd 867 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}})) |
28 | 27 | ord 860 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}})) |
29 | 11, 23, 28 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}}) |
30 | 29 | unieqd 4852 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪
{∅, {𝐴}}) |
31 | | snex 5332 |
. . . . . . 7
⊢ {𝐴} ∈ V |
32 | 5, 31 | unipr 4855 |
. . . . . 6
⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴}) |
33 | | uncom 4129 |
. . . . . 6
⊢ (∅
∪ {𝐴}) = ({𝐴} ∪
∅) |
34 | | un0 4344 |
. . . . . 6
⊢ ({𝐴} ∪ ∅) = {𝐴} |
35 | 32, 33, 34 | 3eqtri 2848 |
. . . . 5
⊢ ∪ {∅, {𝐴}} = {𝐴} |
36 | 30, 35 | syl6eq 2872 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴}) |
37 | | simprrr 780 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤) |
38 | 36, 37 | eqsstrrd 4006 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤) |
39 | | snssg 4717 |
. . . 4
⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤)) |
40 | 39 | biimprd 250 |
. . 3
⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤)) |
41 | 10, 38, 40 | sylc 65 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤) |
42 | | eleq2w 2896 |
. . 3
⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎)) |
43 | | unieq 4849 |
. . . 4
⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪
𝑎) |
44 | 43 | sseq1d 3998 |
. . 3
⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤)) |
45 | 42, 44 | anbi12d 632 |
. 2
⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) |
46 | 8, 41, 45 | rexlimddvcbvw 40608 |
1
⊢ (𝜑 → 𝐴 ∈ 𝑤) |