| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = ∅ → (𝑆‘𝑦) = (𝑆‘∅)) |
| 2 | 1 | eleq2d 2827 |
. . 3
⊢ (𝑦 = ∅ → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘∅))) |
| 3 | 1 | eleq2d 2827 |
. . . . 5
⊢ (𝑦 = ∅ → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
| 4 | 3 | anbi2d 630 |
. . . 4
⊢ (𝑦 = ∅ → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅)))) |
| 5 | 4 | exbidv 1921 |
. . 3
⊢ (𝑦 = ∅ → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅)))) |
| 6 | 2, 5 | bibi12d 345 |
. 2
⊢ (𝑦 = ∅ → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))))) |
| 7 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝑆‘𝑦) = (𝑆‘𝑧)) |
| 8 | 7 | eleq2d 2827 |
. . 3
⊢ (𝑦 = 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑧))) |
| 9 | 7 | eleq2d 2827 |
. . . . 5
⊢ (𝑦 = 𝑧 → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧))) |
| 10 | 9 | anbi2d 630 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) |
| 11 | 10 | exbidv 1921 |
. . 3
⊢ (𝑦 = 𝑧 → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) |
| 12 | 8, 11 | bibi12d 345 |
. 2
⊢ (𝑦 = 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧))))) |
| 13 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = suc 𝑧 → (𝑆‘𝑦) = (𝑆‘suc 𝑧)) |
| 14 | 13 | eleq2d 2827 |
. . 3
⊢ (𝑦 = suc 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘suc 𝑧))) |
| 15 | 13 | eleq2d 2827 |
. . . . 5
⊢ (𝑦 = suc 𝑧 → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧))) |
| 16 | 15 | anbi2d 630 |
. . . 4
⊢ (𝑦 = suc 𝑧 → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
| 17 | 16 | exbidv 1921 |
. . 3
⊢ (𝑦 = suc 𝑧 → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
| 18 | 14, 17 | bibi12d 345 |
. 2
⊢ (𝑦 = suc 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧))))) |
| 19 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = 𝑁 → (𝑆‘𝑦) = (𝑆‘𝑁)) |
| 20 | 19 | eleq2d 2827 |
. . 3
⊢ (𝑦 = 𝑁 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑁))) |
| 21 | 19 | eleq2d 2827 |
. . . . 5
⊢ (𝑦 = 𝑁 → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁))) |
| 22 | 21 | anbi2d 630 |
. . . 4
⊢ (𝑦 = 𝑁 → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) |
| 23 | 22 | exbidv 1921 |
. . 3
⊢ (𝑦 = 𝑁 → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) |
| 24 | 20, 23 | bibi12d 345 |
. 2
⊢ (𝑦 = 𝑁 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁))))) |
| 25 | | satf0op.s |
. . . . . 6
⊢ 𝑆 = (∅ Sat
∅) |
| 26 | 25 | fveq1i 6907 |
. . . . 5
⊢ (𝑆‘∅) = ((∅ Sat
∅)‘∅) |
| 27 | | satf00 35379 |
. . . . 5
⊢ ((∅
Sat ∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
| 28 | 26, 27 | eqtri 2765 |
. . . 4
⊢ (𝑆‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
| 29 | 28 | eleq2i 2833 |
. . 3
⊢ (𝑋 ∈ (𝑆‘∅) ↔ 𝑋 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) |
| 30 | | elopab 5532 |
. . 3
⊢ (𝑋 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ ∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))) |
| 31 | | opeq2 4874 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → 〈𝑥, 𝑦〉 = 〈𝑥, ∅〉) |
| 32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → 〈𝑥, 𝑦〉 = 〈𝑥, ∅〉) |
| 33 | 32 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = 〈𝑥, 𝑦〉 ↔ 𝑋 = 〈𝑥, ∅〉)) |
| 34 | 33 | biimpd 229 |
. . . . . . . 8
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = 〈𝑥, 𝑦〉 → 𝑋 = 〈𝑥, ∅〉)) |
| 35 | 34 | impcom 407 |
. . . . . . 7
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → 𝑋 = 〈𝑥, ∅〉) |
| 36 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ∅ =
∅) |
| 37 | 36 | anim1i 615 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗))) |
| 38 | 37 | adantl 481 |
. . . . . . . 8
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗))) |
| 39 | | satf00 35379 |
. . . . . . . . . . 11
⊢ ((∅
Sat ∅)‘∅) = {〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} |
| 40 | 26, 39 | eqtri 2765 |
. . . . . . . . . 10
⊢ (𝑆‘∅) = {〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} |
| 41 | 40 | eleq2i 2833 |
. . . . . . . . 9
⊢
(〈𝑥,
∅〉 ∈ (𝑆‘∅) ↔ 〈𝑥, ∅〉 ∈
{〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))}) |
| 42 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 43 | | 0ex 5307 |
. . . . . . . . . 10
⊢ ∅
∈ V |
| 44 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ =
∅)) |
| 45 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑖∈𝑔𝑗))) |
| 46 | 45 | 2rexbidv 3222 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) |
| 47 | 44, 46 | bi2anan9r 639 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗)))) |
| 48 | 42, 43, 47 | opelopaba 5541 |
. . . . . . . . 9
⊢
(〈𝑥,
∅〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗))) |
| 49 | 41, 48 | bitri 275 |
. . . . . . . 8
⊢
(〈𝑥,
∅〉 ∈ (𝑆‘∅) ↔ (∅ = ∅
∧ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗))) |
| 50 | 38, 49 | sylibr 234 |
. . . . . . 7
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → 〈𝑥, ∅〉 ∈ (𝑆‘∅)) |
| 51 | 35, 50 | jca 511 |
. . . . . 6
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
| 52 | 51 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
| 53 | 31 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑦 = ∅ → (𝑋 = 〈𝑥, 𝑦〉 ↔ 𝑋 = 〈𝑥, ∅〉)) |
| 54 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ =
∅)) |
| 55 | 54 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗)))) |
| 56 | 53, 55 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = ∅ → ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗))))) |
| 57 | 43, 56 | spcev 3606 |
. . . . . 6
⊢ ((𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗))) → ∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))) |
| 58 | 49, 57 | sylan2b 594 |
. . . . 5
⊢ ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅)) →
∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))) |
| 59 | 52, 58 | impbii 209 |
. . . 4
⊢
(∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
| 60 | 59 | exbii 1848 |
. . 3
⊢
(∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
| 61 | 29, 30, 60 | 3bitri 297 |
. 2
⊢ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
| 62 | 25 | satf0suc 35381 |
. . . . . . 7
⊢ (𝑧 ∈ ω → (𝑆‘suc 𝑧) = ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))})) |
| 63 | 62 | eleq2d 2827 |
. . . . . 6
⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ 𝑋 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
| 64 | | elun 4153 |
. . . . . . 7
⊢ (𝑋 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))})) |
| 65 | 64 | a1i 11 |
. . . . . 6
⊢ (𝑧 ∈ ω → (𝑋 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
| 66 | | elopab 5532 |
. . . . . . . 8
⊢ (𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 67 | 66 | a1i 11 |
. . . . . . 7
⊢ (𝑧 ∈ ω → (𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 68 | 67 | orbi2d 916 |
. . . . . 6
⊢ (𝑧 ∈ ω → ((𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 69 | 63, 65, 68 | 3bitrd 305 |
. . . . 5
⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 70 | 69 | adantr 480 |
. . . 4
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 71 | | simpr 484 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) |
| 72 | | opeq2 4874 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = ∅ → 〈𝑎, 𝑏〉 = 〈𝑎, ∅〉) |
| 73 | 72 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = ∅ → (𝑋 = 〈𝑎, 𝑏〉 ↔ 𝑋 = 〈𝑎, ∅〉)) |
| 74 | 73 | biimpd 229 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ∅ → (𝑋 = 〈𝑎, 𝑏〉 → 𝑋 = 〈𝑎, ∅〉)) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) → (𝑋 = 〈𝑎, 𝑏〉 → 𝑋 = 〈𝑎, ∅〉)) |
| 76 | 75 | impcom 407 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → 𝑋 = 〈𝑎, ∅〉) |
| 77 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → ∅ =
∅) |
| 78 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) → ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) |
| 80 | 77, 79 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) |
| 81 | 76, 80 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 82 | 81 | exlimiv 1930 |
. . . . . . . . . . 11
⊢
(∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 83 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ∅ → (𝑏 = ∅ ↔ ∅ =
∅)) |
| 84 | 83 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 85 | 73, 84 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 86 | 43, 85 | spcev 3606 |
. . . . . . . . . . 11
⊢ ((𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 87 | 82, 86 | impbii 209 |
. . . . . . . . . 10
⊢
(∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 88 | 87 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 89 | 88 | a1i 11 |
. . . . . . . 8
⊢ (𝑧 ∈ ω →
(∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 90 | | opeq1 4873 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → 〈𝑥, ∅〉 = 〈𝑎, ∅〉) |
| 91 | 90 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑋 = 〈𝑥, ∅〉 ↔ 𝑋 = 〈𝑎, ∅〉)) |
| 92 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
| 93 | 92 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
| 94 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) |
| 95 | 94 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑎 =
∀𝑔𝑖(1st ‘𝑢))) |
| 96 | 93, 95 | orbi12d 919 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) |
| 97 | 96 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) |
| 98 | 97 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 99 | 91, 98 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 100 | 99 | cbvexvw 2036 |
. . . . . . . 8
⊢
(∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 101 | 89, 100 | bitr4di 289 |
. . . . . . 7
⊢ (𝑧 ∈ ω →
(∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 102 | 101 | adantr 480 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 103 | 71, 102 | orbi12d 919 |
. . . . 5
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 104 | | 19.43 1882 |
. . . . . 6
⊢
(∃𝑥((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 105 | | andi 1010 |
. . . . . . . 8
⊢ ((𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 106 | 105 | bicomi 224 |
. . . . . . 7
⊢ (((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 107 | 106 | exbii 1848 |
. . . . . 6
⊢
(∃𝑥((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 108 | 104, 107 | bitr3i 277 |
. . . . 5
⊢
((∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 109 | 103, 108 | bitrdi 287 |
. . . 4
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 110 | 62 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑧 ∈ ω →
(〈𝑥, ∅〉
∈ (𝑆‘suc 𝑧) ↔ 〈𝑥, ∅〉 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
| 111 | | elun 4153 |
. . . . . . . . . 10
⊢
(〈𝑥,
∅〉 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ 〈𝑥, ∅〉 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))})) |
| 112 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
| 113 | 112 | rexbidv 3179 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
| 114 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) |
| 115 | 114 | rexbidv 3179 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → (∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑢))) |
| 116 | 113, 115 | orbi12d 919 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑥 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
| 117 | 116 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
| 118 | 83, 117 | bi2anan9r 639 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = ∅) → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 119 | 42, 43, 118 | opelopaba 5541 |
. . . . . . . . . . 11
⊢
(〈𝑥,
∅〉 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
| 120 | 119 | orbi2i 913 |
. . . . . . . . . 10
⊢
((〈𝑥,
∅〉 ∈ (𝑆‘𝑧) ∨ 〈𝑥, ∅〉 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 121 | 111, 120 | bitri 275 |
. . . . . . . . 9
⊢
(〈𝑥,
∅〉 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
| 122 | 110, 121 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑧 ∈ ω →
(〈𝑥, ∅〉
∈ (𝑆‘suc 𝑧) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
| 123 | 122 | anbi2d 630 |
. . . . . . 7
⊢ (𝑧 ∈ ω → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 124 | 123 | exbidv 1921 |
. . . . . 6
⊢ (𝑧 ∈ ω →
(∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
| 125 | 124 | bicomd 223 |
. . . . 5
⊢ (𝑧 ∈ ω →
(∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
| 126 | 125 | adantr 480 |
. . . 4
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
| 127 | 70, 109, 126 | 3bitrd 305 |
. . 3
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
| 128 | 127 | ex 412 |
. 2
⊢ (𝑧 ∈ ω → ((𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧))))) |
| 129 | 6, 12, 18, 24, 61, 128 | finds 7918 |
1
⊢ (𝑁 ∈ ω → (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) |