Step | Hyp | Ref
| Expression |
1 | | fveq2 6776 |
. . . 4
⊢ (𝑦 = ∅ → (𝑆‘𝑦) = (𝑆‘∅)) |
2 | 1 | eleq2d 2824 |
. . 3
⊢ (𝑦 = ∅ → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘∅))) |
3 | 1 | eleq2d 2824 |
. . . . 5
⊢ (𝑦 = ∅ → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
4 | 3 | anbi2d 629 |
. . . 4
⊢ (𝑦 = ∅ → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅)))) |
5 | 4 | exbidv 1924 |
. . 3
⊢ (𝑦 = ∅ → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅)))) |
6 | 2, 5 | bibi12d 346 |
. 2
⊢ (𝑦 = ∅ → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))))) |
7 | | fveq2 6776 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝑆‘𝑦) = (𝑆‘𝑧)) |
8 | 7 | eleq2d 2824 |
. . 3
⊢ (𝑦 = 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑧))) |
9 | 7 | eleq2d 2824 |
. . . . 5
⊢ (𝑦 = 𝑧 → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧))) |
10 | 9 | anbi2d 629 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) |
11 | 10 | exbidv 1924 |
. . 3
⊢ (𝑦 = 𝑧 → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) |
12 | 8, 11 | bibi12d 346 |
. 2
⊢ (𝑦 = 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧))))) |
13 | | fveq2 6776 |
. . . 4
⊢ (𝑦 = suc 𝑧 → (𝑆‘𝑦) = (𝑆‘suc 𝑧)) |
14 | 13 | eleq2d 2824 |
. . 3
⊢ (𝑦 = suc 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘suc 𝑧))) |
15 | 13 | eleq2d 2824 |
. . . . 5
⊢ (𝑦 = suc 𝑧 → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧))) |
16 | 15 | anbi2d 629 |
. . . 4
⊢ (𝑦 = suc 𝑧 → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
17 | 16 | exbidv 1924 |
. . 3
⊢ (𝑦 = suc 𝑧 → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
18 | 14, 17 | bibi12d 346 |
. 2
⊢ (𝑦 = suc 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧))))) |
19 | | fveq2 6776 |
. . . 4
⊢ (𝑦 = 𝑁 → (𝑆‘𝑦) = (𝑆‘𝑁)) |
20 | 19 | eleq2d 2824 |
. . 3
⊢ (𝑦 = 𝑁 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑁))) |
21 | 19 | eleq2d 2824 |
. . . . 5
⊢ (𝑦 = 𝑁 → (〈𝑥, ∅〉 ∈ (𝑆‘𝑦) ↔ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁))) |
22 | 21 | anbi2d 629 |
. . . 4
⊢ (𝑦 = 𝑁 → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) |
23 | 22 | exbidv 1924 |
. . 3
⊢ (𝑦 = 𝑁 → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) |
24 | 20, 23 | bibi12d 346 |
. 2
⊢ (𝑦 = 𝑁 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁))))) |
25 | | satf0op.s |
. . . . . 6
⊢ 𝑆 = (∅ Sat
∅) |
26 | 25 | fveq1i 6777 |
. . . . 5
⊢ (𝑆‘∅) = ((∅ Sat
∅)‘∅) |
27 | | satf00 33333 |
. . . . 5
⊢ ((∅
Sat ∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
28 | 26, 27 | eqtri 2766 |
. . . 4
⊢ (𝑆‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
29 | 28 | eleq2i 2830 |
. . 3
⊢ (𝑋 ∈ (𝑆‘∅) ↔ 𝑋 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) |
30 | | elopab 5442 |
. . 3
⊢ (𝑋 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ ∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))) |
31 | | opeq2 4807 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → 〈𝑥, 𝑦〉 = 〈𝑥, ∅〉) |
32 | 31 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → 〈𝑥, 𝑦〉 = 〈𝑥, ∅〉) |
33 | 32 | eqeq2d 2749 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = 〈𝑥, 𝑦〉 ↔ 𝑋 = 〈𝑥, ∅〉)) |
34 | 33 | biimpd 228 |
. . . . . . . 8
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = 〈𝑥, 𝑦〉 → 𝑋 = 〈𝑥, ∅〉)) |
35 | 34 | impcom 408 |
. . . . . . 7
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → 𝑋 = 〈𝑥, ∅〉) |
36 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ∅ =
∅) |
37 | 36 | anim1i 615 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗))) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗))) |
39 | | satf00 33333 |
. . . . . . . . . . 11
⊢ ((∅
Sat ∅)‘∅) = {〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} |
40 | 26, 39 | eqtri 2766 |
. . . . . . . . . 10
⊢ (𝑆‘∅) = {〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} |
41 | 40 | eleq2i 2830 |
. . . . . . . . 9
⊢
(〈𝑥,
∅〉 ∈ (𝑆‘∅) ↔ 〈𝑥, ∅〉 ∈
{〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))}) |
42 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
43 | | 0ex 5233 |
. . . . . . . . . 10
⊢ ∅
∈ V |
44 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ =
∅)) |
45 | | eqeq1 2742 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑖∈𝑔𝑗))) |
46 | 45 | 2rexbidv 3228 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) |
47 | 44, 46 | bi2anan9r 637 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗)))) |
48 | 42, 43, 47 | opelopaba 5451 |
. . . . . . . . 9
⊢
(〈𝑥,
∅〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗))) |
49 | 41, 48 | bitri 274 |
. . . . . . . 8
⊢
(〈𝑥,
∅〉 ∈ (𝑆‘∅) ↔ (∅ = ∅
∧ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗))) |
50 | 38, 49 | sylibr 233 |
. . . . . . 7
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → 〈𝑥, ∅〉 ∈ (𝑆‘∅)) |
51 | 35, 50 | jca 512 |
. . . . . 6
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
52 | 51 | exlimiv 1933 |
. . . . 5
⊢
(∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
53 | 31 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑦 = ∅ → (𝑋 = 〈𝑥, 𝑦〉 ↔ 𝑋 = 〈𝑥, ∅〉)) |
54 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ =
∅)) |
55 | 54 | anbi1d 630 |
. . . . . . . 8
⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗)))) |
56 | 53, 55 | anbi12d 631 |
. . . . . . 7
⊢ (𝑦 = ∅ → ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗))))) |
57 | 43, 56 | spcev 3544 |
. . . . . 6
⊢ ((𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗))) → ∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))) |
58 | 49, 57 | sylan2b 594 |
. . . . 5
⊢ ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅)) →
∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))) |
59 | 52, 58 | impbii 208 |
. . . 4
⊢
(∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
60 | 59 | exbii 1850 |
. . 3
⊢
(∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
61 | 29, 30, 60 | 3bitri 297 |
. 2
⊢ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘∅))) |
62 | 25 | satf0suc 33335 |
. . . . . . 7
⊢ (𝑧 ∈ ω → (𝑆‘suc 𝑧) = ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))})) |
63 | 62 | eleq2d 2824 |
. . . . . 6
⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ 𝑋 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
64 | | elun 4084 |
. . . . . . 7
⊢ (𝑋 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))})) |
65 | 64 | a1i 11 |
. . . . . 6
⊢ (𝑧 ∈ ω → (𝑋 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
66 | | elopab 5442 |
. . . . . . . 8
⊢ (𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
67 | 66 | a1i 11 |
. . . . . . 7
⊢ (𝑧 ∈ ω → (𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
68 | 67 | orbi2d 913 |
. . . . . 6
⊢ (𝑧 ∈ ω → ((𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))))) |
69 | 63, 65, 68 | 3bitrd 305 |
. . . . 5
⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))))) |
70 | 69 | adantr 481 |
. . . 4
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))))) |
71 | | simpr 485 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) |
72 | | opeq2 4807 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = ∅ → 〈𝑎, 𝑏〉 = 〈𝑎, ∅〉) |
73 | 72 | eqeq2d 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = ∅ → (𝑋 = 〈𝑎, 𝑏〉 ↔ 𝑋 = 〈𝑎, ∅〉)) |
74 | 73 | biimpd 228 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ∅ → (𝑋 = 〈𝑎, 𝑏〉 → 𝑋 = 〈𝑎, ∅〉)) |
75 | 74 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) → (𝑋 = 〈𝑎, 𝑏〉 → 𝑋 = 〈𝑎, ∅〉)) |
76 | 75 | impcom 408 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → 𝑋 = 〈𝑎, ∅〉) |
77 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → ∅ =
∅) |
78 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) → ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) |
79 | 78 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) |
80 | 77, 79 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) |
81 | 76, 80 | jca 512 |
. . . . . . . . . . . 12
⊢ ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
82 | 81 | exlimiv 1933 |
. . . . . . . . . . 11
⊢
(∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
83 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ∅ → (𝑏 = ∅ ↔ ∅ =
∅)) |
84 | 83 | anbi1d 630 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
85 | 73, 84 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → ((𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
86 | 43, 85 | spcev 3544 |
. . . . . . . . . . 11
⊢ ((𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
87 | 82, 86 | impbii 208 |
. . . . . . . . . 10
⊢
(∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
88 | 87 | exbii 1850 |
. . . . . . . . 9
⊢
(∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
89 | 88 | a1i 11 |
. . . . . . . 8
⊢ (𝑧 ∈ ω →
(∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
90 | | opeq1 4806 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → 〈𝑥, ∅〉 = 〈𝑎, ∅〉) |
91 | 90 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑋 = 〈𝑥, ∅〉 ↔ 𝑋 = 〈𝑎, ∅〉)) |
92 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
93 | 92 | rexbidv 3225 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
94 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) |
95 | 94 | rexbidv 3225 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑎 =
∀𝑔𝑖(1st ‘𝑢))) |
96 | 93, 95 | orbi12d 916 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) |
97 | 96 | rexbidv 3225 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) |
98 | 97 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
99 | 91, 98 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))))) |
100 | 99 | cbvexvw 2040 |
. . . . . . . 8
⊢
(∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = 〈𝑎, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) |
101 | 89, 100 | bitr4di 289 |
. . . . . . 7
⊢ (𝑧 ∈ ω →
(∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
102 | 101 | adantr 481 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
103 | 71, 102 | orbi12d 916 |
. . . . 5
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
104 | | 19.43 1885 |
. . . . . 6
⊢
(∃𝑥((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
105 | | andi 1005 |
. . . . . . . 8
⊢ ((𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
106 | 105 | bicomi 223 |
. . . . . . 7
⊢ (((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
107 | 106 | exbii 1850 |
. . . . . 6
⊢
(∃𝑥((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ (𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
108 | 104, 107 | bitr3i 276 |
. . . . 5
⊢
((∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (∅ = ∅
∧ ∃𝑢 ∈
(𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
109 | 103, 108 | bitrdi 287 |
. . . 4
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = 〈𝑎, 𝑏〉 ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
110 | 62 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝑧 ∈ ω →
(〈𝑥, ∅〉
∈ (𝑆‘suc 𝑧) ↔ 〈𝑥, ∅〉 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
111 | | elun 4084 |
. . . . . . . . . 10
⊢
(〈𝑥,
∅〉 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ 〈𝑥, ∅〉 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))})) |
112 | | eqeq1 2742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
113 | 112 | rexbidv 3225 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
114 | | eqeq1 2742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) |
115 | 114 | rexbidv 3225 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → (∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑢))) |
116 | 113, 115 | orbi12d 916 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑥 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
117 | 116 | rexbidv 3225 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
118 | 83, 117 | bi2anan9r 637 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = ∅) → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
119 | 42, 43, 118 | opelopaba 5451 |
. . . . . . . . . . 11
⊢
(〈𝑥,
∅〉 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧
∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
120 | 119 | orbi2i 910 |
. . . . . . . . . 10
⊢
((〈𝑥,
∅〉 ∈ (𝑆‘𝑧) ∨ 〈𝑥, ∅〉 ∈ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
121 | 111, 120 | bitri 274 |
. . . . . . . . 9
⊢
(〈𝑥,
∅〉 ∈ ((𝑆‘𝑧) ∪ {〈𝑎, 𝑏〉 ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑎 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
122 | 110, 121 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑧 ∈ ω →
(〈𝑥, ∅〉
∈ (𝑆‘suc 𝑧) ↔ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))))) |
123 | 122 | anbi2d 629 |
. . . . . . 7
⊢ (𝑧 ∈ ω → ((𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)) ↔ (𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
124 | 123 | exbidv 1924 |
. . . . . 6
⊢ (𝑧 ∈ ω →
(∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))))) |
125 | 124 | bicomd 222 |
. . . . 5
⊢ (𝑧 ∈ ω →
(∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
126 | 125 | adantr 481 |
. . . 4
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ (〈𝑥, ∅〉 ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
127 | 70, 109, 126 | 3bitrd 305 |
. . 3
⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧)))) |
128 | 127 | ex 413 |
. 2
⊢ (𝑧 ∈ ω → ((𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑧))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘suc 𝑧))))) |
129 | 6, 12, 18, 24, 61, 128 | finds 7745 |
1
⊢ (𝑁 ∈ ω → (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) |