| Step | Hyp | Ref
| Expression |
| 1 | | fmla0 35387 |
. . . 4
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} |
| 2 | | rabab 3512 |
. . . 4
⊢ {𝑥 ∈ V ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} = {𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} |
| 3 | 1, 2 | eqtri 2765 |
. . 3
⊢
(Fmla‘∅) = {𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} |
| 4 | 3 | ineq1i 4216 |
. 2
⊢
((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) |
| 5 | | inab 4309 |
. . 3
⊢ ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = {𝑥 ∣ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))} |
| 6 | | goel 35352 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑗∈𝑔𝑘) = 〈∅, 〈𝑗, 𝑘〉〉) |
| 7 | 6 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗∈𝑔𝑘) ↔ 𝑥 = 〈∅, 〈𝑗, 𝑘〉〉)) |
| 8 | | 1n0 8526 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1o ≠ ∅ |
| 9 | 8 | nesymi 2998 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
∅ = 1o |
| 10 | 9 | intnanr 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
(∅ = 1o ∧ 〈𝑗, 𝑘〉 = 〈𝑢, 𝑣〉) |
| 11 | | gonafv 35355 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢⊼𝑔𝑣) = 〈1o,
〈𝑢, 𝑣〉〉) |
| 12 | 11 | el2v 3487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢⊼𝑔𝑣) = 〈1o,
〈𝑢, 𝑣〉〉 |
| 13 | 12 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈∅, 〈𝑗, 𝑘〉〉 = (𝑢⊼𝑔𝑣) ↔ 〈∅, 〈𝑗, 𝑘〉〉 = 〈1o,
〈𝑢, 𝑣〉〉) |
| 14 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ V |
| 15 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈𝑗, 𝑘〉 ∈ V |
| 16 | 14, 15 | opth 5481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈∅, 〈𝑗, 𝑘〉〉 = 〈1o,
〈𝑢, 𝑣〉〉 ↔ (∅ = 1o
∧ 〈𝑗, 𝑘〉 = 〈𝑢, 𝑣〉)) |
| 17 | 13, 16 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈∅, 〈𝑗, 𝑘〉〉 = (𝑢⊼𝑔𝑣) ↔ (∅ = 1o ∧
〈𝑗, 𝑘〉 = 〈𝑢, 𝑣〉)) |
| 18 | 10, 17 | mtbir 323 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
〈∅, 〈𝑗,
𝑘〉〉 = (𝑢⊼𝑔𝑣) |
| 19 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 〈∅, 〈𝑗, 𝑘〉〉 → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 〈∅, 〈𝑗, 𝑘〉〉 = (𝑢⊼𝑔𝑣))) |
| 20 | 18, 19 | mtbiri 327 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 〈∅, 〈𝑗, 𝑘〉〉 → ¬ 𝑥 = (𝑢⊼𝑔𝑣)) |
| 21 | 7, 20 | biimtrdi 253 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗∈𝑔𝑘) → ¬ 𝑥 = (𝑢⊼𝑔𝑣))) |
| 22 | 21 | imp 406 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) → ¬ 𝑥 = (𝑢⊼𝑔𝑣)) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ¬
𝑥 = (𝑢⊼𝑔𝑣)) |
| 24 | 23 | ralrimivw 3150 |
. . . . . . . . . . . 12
⊢ ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) →
∀𝑣 ∈
(Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣)) |
| 25 | | 2on0 8522 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
2o ≠ ∅ |
| 26 | 25 | nesymi 2998 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ¬
∅ = 2o |
| 27 | 26 | orci 866 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∅ = 2o ∨ ¬ 〈𝑗, 𝑘〉 = 〈𝑖, 𝑢〉) |
| 28 | 14, 15 | opth 5481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈∅, 〈𝑗, 𝑘〉〉 = 〈2o,
〈𝑖, 𝑢〉〉 ↔ (∅ = 2o
∧ 〈𝑗, 𝑘〉 = 〈𝑖, 𝑢〉)) |
| 29 | 28 | notbii 320 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
〈∅, 〈𝑗,
𝑘〉〉 =
〈2o, 〈𝑖, 𝑢〉〉 ↔ ¬ (∅ =
2o ∧ 〈𝑗, 𝑘〉 = 〈𝑖, 𝑢〉)) |
| 30 | | ianor 984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(∅ = 2o ∧ 〈𝑗, 𝑘〉 = 〈𝑖, 𝑢〉) ↔ (¬ ∅ = 2o
∨ ¬ 〈𝑗, 𝑘〉 = 〈𝑖, 𝑢〉)) |
| 31 | 29, 30 | bitri 275 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
〈∅, 〈𝑗,
𝑘〉〉 =
〈2o, 〈𝑖, 𝑢〉〉 ↔ (¬ ∅ =
2o ∨ ¬ 〈𝑗, 𝑘〉 = 〈𝑖, 𝑢〉)) |
| 32 | 27, 31 | mpbir 231 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
〈∅, 〈𝑗,
𝑘〉〉 =
〈2o, 〈𝑖, 𝑢〉〉 |
| 33 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 〈∅, 〈𝑗, 𝑘〉〉 → (𝑥 = ∀𝑔𝑖𝑢 ↔ 〈∅, 〈𝑗, 𝑘〉〉 =
∀𝑔𝑖𝑢)) |
| 34 | | df-goal 35347 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑔𝑖𝑢 = 〈2o, 〈𝑖, 𝑢〉〉 |
| 35 | 34 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈∅, 〈𝑗, 𝑘〉〉 =
∀𝑔𝑖𝑢 ↔ 〈∅, 〈𝑗, 𝑘〉〉 = 〈2o,
〈𝑖, 𝑢〉〉) |
| 36 | 33, 35 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈∅, 〈𝑗, 𝑘〉〉 → (𝑥 = ∀𝑔𝑖𝑢 ↔ 〈∅, 〈𝑗, 𝑘〉〉 = 〈2o,
〈𝑖, 𝑢〉〉)) |
| 37 | 32, 36 | mtbiri 327 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 〈∅, 〈𝑗, 𝑘〉〉 → ¬ 𝑥 = ∀𝑔𝑖𝑢) |
| 38 | 7, 37 | biimtrdi 253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗∈𝑔𝑘) → ¬ 𝑥 = ∀𝑔𝑖𝑢)) |
| 39 | 38 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) → ¬ 𝑥 = ∀𝑔𝑖𝑢) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ¬
𝑥 =
∀𝑔𝑖𝑢) |
| 41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑗 ∈
ω ∧ 𝑘 ∈
ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) ∧ 𝑖 ∈ ω) → ¬
𝑥 =
∀𝑔𝑖𝑢) |
| 42 | 41 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) →
∀𝑖 ∈ ω
¬ 𝑥 =
∀𝑔𝑖𝑢) |
| 43 | 24, 42 | jca 511 |
. . . . . . . . . . 11
⊢ ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) →
(∀𝑣 ∈
(Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢)) |
| 44 | 43 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) → ∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅)
¬ 𝑥 = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 =
∀𝑔𝑖𝑢)) |
| 45 | | ralnex 3072 |
. . . . . . . . . . . . . 14
⊢
(∀𝑣 ∈
(Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣) ↔ ¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣)) |
| 46 | | ralnex 3072 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
ω ¬ 𝑥 =
∀𝑔𝑖𝑢 ↔ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) |
| 47 | 45, 46 | anbi12i 628 |
. . . . . . . . . . . . 13
⊢
((∀𝑣 ∈
(Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 48 | | ioran 986 |
. . . . . . . . . . . . 13
⊢ (¬
(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 49 | 47, 48 | bitr4i 278 |
. . . . . . . . . . . 12
⊢
((∀𝑣 ∈
(Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 50 | 49 | ralbii 3093 |
. . . . . . . . . . 11
⊢
(∀𝑢 ∈
(Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ∀𝑢 ∈ (Fmla‘∅) ¬
(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 51 | | ralnex 3072 |
. . . . . . . . . . 11
⊢
(∀𝑢 ∈
(Fmla‘∅) ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 52 | 50, 51 | bitri 275 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
(Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 53 | 44, 52 | sylib 218 |
. . . . . . . . 9
⊢ (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗∈𝑔𝑘)) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 54 | 53 | ex 412 |
. . . . . . . 8
⊢ ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗∈𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
| 55 | 54 | rexlimdva 3155 |
. . . . . . 7
⊢ (𝑗 ∈ ω →
(∃𝑘 ∈ ω
𝑥 = (𝑗∈𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
| 56 | 55 | rexlimiv 3148 |
. . . . . 6
⊢
(∃𝑗 ∈
ω ∃𝑘 ∈
ω 𝑥 = (𝑗∈𝑔𝑘) → ¬ ∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 57 | 56 | imori 855 |
. . . . 5
⊢ (¬
∃𝑗 ∈ ω
∃𝑘 ∈ ω
𝑥 = (𝑗∈𝑔𝑘) ∨ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 58 | | ianor 984 |
. . . . 5
⊢ (¬
(∃𝑗 ∈ ω
∃𝑘 ∈ ω
𝑥 = (𝑗∈𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ↔ (¬ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘) ∨ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
| 59 | 57, 58 | mpbir 231 |
. . . 4
⊢ ¬
(∃𝑗 ∈ ω
∃𝑘 ∈ ω
𝑥 = (𝑗∈𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 60 | 59 | abf 4406 |
. . 3
⊢ {𝑥 ∣ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))} = ∅ |
| 61 | 5, 60 | eqtri 2765 |
. 2
⊢ ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗∈𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅ |
| 62 | 4, 61 | eqtri 2765 |
1
⊢
((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)𝑥 =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅ |