Step | Hyp | Ref
| Expression |
1 | | mnuprdlem3.9 |
. 2
⊢
Ⅎ𝑖𝜑 |
2 | | elpri 4563 |
. . . . 5
⊢ (𝑖 ∈ {∅, {∅}}
→ (𝑖 = ∅ ∨
𝑖 =
{∅})) |
3 | | 0ex 5200 |
. . . . . . . . . 10
⊢ ∅
∈ V |
4 | 3 | prid1 4678 |
. . . . . . . . 9
⊢ ∅
∈ {∅, {𝐴}} |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → ∅ ∈ {∅, {𝐴}}) |
6 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 = ∅) |
7 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑎 = {∅, {𝐴}}) |
8 | 5, 6, 7 | 3eltr4d 2853 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 ∈ 𝑎) |
9 | | prex 5325 |
. . . . . . . . . 10
⊢ {∅,
{𝐴}} ∈
V |
10 | 9 | prid1 4678 |
. . . . . . . . 9
⊢ {∅,
{𝐴}} ∈ {{∅,
{𝐴}}, {{∅}, {𝐵}}} |
11 | | mnuprdlem3.1 |
. . . . . . . . 9
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} |
12 | 10, 11 | eleqtrri 2837 |
. . . . . . . 8
⊢ {∅,
{𝐴}} ∈ 𝐹 |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = ∅) → {∅, {𝐴}} ∈ 𝐹) |
14 | 8, 13 | rspcime 3541 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = ∅) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎) |
15 | | p0ex 5277 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
16 | 15 | prid1 4678 |
. . . . . . . . 9
⊢ {∅}
∈ {{∅}, {𝐵}} |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → {∅} ∈ {{∅},
{𝐵}}) |
18 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 = {∅}) |
19 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑎 = {{∅}, {𝐵}}) |
20 | 17, 18, 19 | 3eltr4d 2853 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 ∈ 𝑎) |
21 | | prex 5325 |
. . . . . . . . . 10
⊢
{{∅}, {𝐵}}
∈ V |
22 | 21 | prid2 4679 |
. . . . . . . . 9
⊢
{{∅}, {𝐵}}
∈ {{∅, {𝐴}},
{{∅}, {𝐵}}} |
23 | 22, 11 | eleqtrri 2837 |
. . . . . . . 8
⊢
{{∅}, {𝐵}}
∈ 𝐹 |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = {∅}) → {{∅}, {𝐵}} ∈ 𝐹) |
25 | 20, 24 | rspcime 3541 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = {∅}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎) |
26 | 14, 25 | jaodan 958 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 = ∅ ∨ 𝑖 = {∅})) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎) |
27 | 2, 26 | sylan2 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) →
∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎) |
28 | | elequ2 2125 |
. . . . 5
⊢ (𝑎 = 𝑣 → (𝑖 ∈ 𝑎 ↔ 𝑖 ∈ 𝑣)) |
29 | 28 | cbvrexvw 3359 |
. . . 4
⊢
(∃𝑎 ∈
𝐹 𝑖 ∈ 𝑎 ↔ ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) |
30 | 27, 29 | sylib 221 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) →
∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) |
31 | 30 | ex 416 |
. 2
⊢ (𝜑 → (𝑖 ∈ {∅, {∅}} →
∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)) |
32 | 1, 31 | ralrimi 3137 |
1
⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) |