Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  satf0op Structured version   Visualization version   GIF version

Theorem satf0op 32738
Description: An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023.)
Hypothesis
Ref Expression
satf0op.s 𝑆 = (∅ Sat ∅)
Assertion
Ref Expression
satf0op (𝑁 ∈ ω → (𝑋 ∈ (𝑆𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑁))))
Distinct variable groups:   𝑥,𝑁   𝑥,𝑆   𝑥,𝑋

Proof of Theorem satf0op
Dummy variables 𝑖 𝑗 𝑦 𝑧 𝑎 𝑏 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6649 . . . 4 (𝑦 = ∅ → (𝑆𝑦) = (𝑆‘∅))
21eleq2d 2878 . . 3 (𝑦 = ∅ → (𝑋 ∈ (𝑆𝑦) ↔ 𝑋 ∈ (𝑆‘∅)))
31eleq2d 2878 . . . . 5 (𝑦 = ∅ → (⟨𝑥, ∅⟩ ∈ (𝑆𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
43anbi2d 631 . . . 4 (𝑦 = ∅ → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))))
54exbidv 1922 . . 3 (𝑦 = ∅ → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))))
62, 5bibi12d 349 . 2 (𝑦 = ∅ → ((𝑋 ∈ (𝑆𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦))) ↔ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))))
7 fveq2 6649 . . . 4 (𝑦 = 𝑧 → (𝑆𝑦) = (𝑆𝑧))
87eleq2d 2878 . . 3 (𝑦 = 𝑧 → (𝑋 ∈ (𝑆𝑦) ↔ 𝑋 ∈ (𝑆𝑧)))
97eleq2d 2878 . . . . 5 (𝑦 = 𝑧 → (⟨𝑥, ∅⟩ ∈ (𝑆𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))
109anbi2d 631 . . . 4 (𝑦 = 𝑧 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧))))
1110exbidv 1922 . . 3 (𝑦 = 𝑧 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧))))
128, 11bibi12d 349 . 2 (𝑦 = 𝑧 → ((𝑋 ∈ (𝑆𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦))) ↔ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))))
13 fveq2 6649 . . . 4 (𝑦 = suc 𝑧 → (𝑆𝑦) = (𝑆‘suc 𝑧))
1413eleq2d 2878 . . 3 (𝑦 = suc 𝑧 → (𝑋 ∈ (𝑆𝑦) ↔ 𝑋 ∈ (𝑆‘suc 𝑧)))
1513eleq2d 2878 . . . . 5 (𝑦 = suc 𝑧 → (⟨𝑥, ∅⟩ ∈ (𝑆𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))
1615anbi2d 631 . . . 4 (𝑦 = suc 𝑧 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
1716exbidv 1922 . . 3 (𝑦 = suc 𝑧 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
1814, 17bibi12d 349 . 2 (𝑦 = suc 𝑧 → ((𝑋 ∈ (𝑆𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦))) ↔ (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))))
19 fveq2 6649 . . . 4 (𝑦 = 𝑁 → (𝑆𝑦) = (𝑆𝑁))
2019eleq2d 2878 . . 3 (𝑦 = 𝑁 → (𝑋 ∈ (𝑆𝑦) ↔ 𝑋 ∈ (𝑆𝑁)))
2119eleq2d 2878 . . . . 5 (𝑦 = 𝑁 → (⟨𝑥, ∅⟩ ∈ (𝑆𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆𝑁)))
2221anbi2d 631 . . . 4 (𝑦 = 𝑁 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑁))))
2322exbidv 1922 . . 3 (𝑦 = 𝑁 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑁))))
2420, 23bibi12d 349 . 2 (𝑦 = 𝑁 → ((𝑋 ∈ (𝑆𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑦))) ↔ (𝑋 ∈ (𝑆𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑁)))))
25 satf0op.s . . . . . 6 𝑆 = (∅ Sat ∅)
2625fveq1i 6650 . . . . 5 (𝑆‘∅) = ((∅ Sat ∅)‘∅)
27 satf00 32735 . . . . 5 ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))}
2826, 27eqtri 2824 . . . 4 (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))}
2928eleq2i 2884 . . 3 (𝑋 ∈ (𝑆‘∅) ↔ 𝑋 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})
30 elopab 5382 . . 3 (𝑋 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))} ↔ ∃𝑥𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))))
31 opeq2 4768 . . . . . . . . . . 11 (𝑦 = ∅ → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∅⟩)
3231adantr 484 . . . . . . . . . 10 ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∅⟩)
3332eqeq2d 2812 . . . . . . . . 9 ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)) → (𝑋 = ⟨𝑥, 𝑦⟩ ↔ 𝑋 = ⟨𝑥, ∅⟩))
3433biimpd 232 . . . . . . . 8 ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)) → (𝑋 = ⟨𝑥, 𝑦⟩ → 𝑋 = ⟨𝑥, ∅⟩))
3534impcom 411 . . . . . . 7 ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) → 𝑋 = ⟨𝑥, ∅⟩)
36 eqidd 2802 . . . . . . . . . 10 (𝑦 = ∅ → ∅ = ∅)
3736anim1i 617 . . . . . . . . 9 ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)) → (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)))
3837adantl 485 . . . . . . . 8 ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) → (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)))
39 satf00 32735 . . . . . . . . . . 11 ((∅ Sat ∅)‘∅) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖𝑔𝑗))}
4026, 39eqtri 2824 . . . . . . . . . 10 (𝑆‘∅) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖𝑔𝑗))}
4140eleq2i 2884 . . . . . . . . 9 (⟨𝑥, ∅⟩ ∈ (𝑆‘∅) ↔ ⟨𝑥, ∅⟩ ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖𝑔𝑗))})
42 vex 3447 . . . . . . . . . 10 𝑥 ∈ V
43 0ex 5178 . . . . . . . . . 10 ∅ ∈ V
44 eqeq1 2805 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ = ∅))
45 eqeq1 2805 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑦 = (𝑖𝑔𝑗) ↔ 𝑥 = (𝑖𝑔𝑗)))
46452rexbidv 3262 . . . . . . . . . . 11 (𝑦 = 𝑥 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)))
4744, 46bi2anan9r 639 . . . . . . . . . 10 ((𝑦 = 𝑥𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖𝑔𝑗)) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))))
4842, 43, 47opelopaba 5391 . . . . . . . . 9 (⟨𝑥, ∅⟩ ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖𝑔𝑗))} ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)))
4941, 48bitri 278 . . . . . . . 8 (⟨𝑥, ∅⟩ ∈ (𝑆‘∅) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)))
5038, 49sylibr 237 . . . . . . 7 ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) → ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))
5135, 50jca 515 . . . . . 6 ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) → (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
5251exlimiv 1931 . . . . 5 (∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) → (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
5331eqeq2d 2812 . . . . . . . 8 (𝑦 = ∅ → (𝑋 = ⟨𝑥, 𝑦⟩ ↔ 𝑋 = ⟨𝑥, ∅⟩))
54 eqeq1 2805 . . . . . . . . 9 (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ = ∅))
5554anbi1d 632 . . . . . . . 8 (𝑦 = ∅ → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))))
5653, 55anbi12d 633 . . . . . . 7 (𝑦 = ∅ → ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)))))
5743, 56spcev 3558 . . . . . 6 ((𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) → ∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))))
5849, 57sylan2b 596 . . . . 5 ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)) → ∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))))
5952, 58impbii 212 . . . 4 (∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
6059exbii 1849 . . 3 (∃𝑥𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
6129, 30, 603bitri 300 . 2 (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
6225satf0suc 32737 . . . . . . 7 (𝑧 ∈ ω → (𝑆‘suc 𝑧) = ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}))
6362eleq2d 2878 . . . . . 6 (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ 𝑋 ∈ ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))})))
64 elun 4079 . . . . . . 7 (𝑋 ∈ ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}) ↔ (𝑋 ∈ (𝑆𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}))
6564a1i 11 . . . . . 6 (𝑧 ∈ ω → (𝑋 ∈ ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}) ↔ (𝑋 ∈ (𝑆𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))})))
66 elopab 5382 . . . . . . . 8 (𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))} ↔ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
6766a1i 11 . . . . . . 7 (𝑧 ∈ ω → (𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))} ↔ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))))
6867orbi2d 913 . . . . . 6 (𝑧 ∈ ω → ((𝑋 ∈ (𝑆𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}) ↔ (𝑋 ∈ (𝑆𝑧) ∨ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))))
6963, 65, 683bitrd 308 . . . . 5 (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆𝑧) ∨ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))))
7069adantr 484 . . . 4 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆𝑧) ∨ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))))
71 simpr 488 . . . . . 6 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧))))
72 opeq2 4768 . . . . . . . . . . . . . . . . 17 (𝑏 = ∅ → ⟨𝑎, 𝑏⟩ = ⟨𝑎, ∅⟩)
7372eqeq2d 2812 . . . . . . . . . . . . . . . 16 (𝑏 = ∅ → (𝑋 = ⟨𝑎, 𝑏⟩ ↔ 𝑋 = ⟨𝑎, ∅⟩))
7473biimpd 232 . . . . . . . . . . . . . . 15 (𝑏 = ∅ → (𝑋 = ⟨𝑎, 𝑏⟩ → 𝑋 = ⟨𝑎, ∅⟩))
7574adantr 484 . . . . . . . . . . . . . 14 ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))) → (𝑋 = ⟨𝑎, 𝑏⟩ → 𝑋 = ⟨𝑎, ∅⟩))
7675impcom 411 . . . . . . . . . . . . 13 ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → 𝑋 = ⟨𝑎, ∅⟩)
77 eqidd 2802 . . . . . . . . . . . . . 14 ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → ∅ = ∅)
78 simpr 488 . . . . . . . . . . . . . . 15 ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))) → ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))
7978adantl 485 . . . . . . . . . . . . . 14 ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))
8077, 79jca 515 . . . . . . . . . . . . 13 ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))
8176, 80jca 515 . . . . . . . . . . . 12 ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
8281exlimiv 1931 . . . . . . . . . . 11 (∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
83 eqeq1 2805 . . . . . . . . . . . . . 14 (𝑏 = ∅ → (𝑏 = ∅ ↔ ∅ = ∅))
8483anbi1d 632 . . . . . . . . . . . . 13 (𝑏 = ∅ → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
8573, 84anbi12d 633 . . . . . . . . . . . 12 (𝑏 = ∅ → ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) ↔ (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))))
8643, 85spcev 3558 . . . . . . . . . . 11 ((𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) → ∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
8782, 86impbii 212 . . . . . . . . . 10 (∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) ↔ (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
8887exbii 1849 . . . . . . . . 9 (∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) ↔ ∃𝑎(𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
8988a1i 11 . . . . . . . 8 (𝑧 ∈ ω → (∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) ↔ ∃𝑎(𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))))
90 opeq1 4766 . . . . . . . . . . 11 (𝑥 = 𝑎 → ⟨𝑥, ∅⟩ = ⟨𝑎, ∅⟩)
9190eqeq2d 2812 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑋 = ⟨𝑥, ∅⟩ ↔ 𝑋 = ⟨𝑎, ∅⟩))
92 eqeq1 2805 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑎 = ((1st𝑢)⊼𝑔(1st𝑣))))
9392rexbidv 3259 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣))))
94 eqeq1 2805 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ 𝑎 = ∀𝑔𝑖(1st𝑢)))
9594rexbidv 3259 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢) ↔ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))
9693, 95orbi12d 916 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) ↔ (∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))
9796rexbidv 3259 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) ↔ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))
9897anbi2d 631 . . . . . . . . . 10 (𝑥 = 𝑎 → ((∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
9991, 98anbi12d 633 . . . . . . . . 9 (𝑥 = 𝑎 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))) ↔ (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))))
10099cbvexvw 2044 . . . . . . . 8 (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))) ↔ ∃𝑎(𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))))
10189, 100syl6bbr 292 . . . . . . 7 (𝑧 ∈ ω → (∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
102101adantr 484 . . . . . 6 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → (∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
10371, 102orbi12d 916 . . . . 5 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → ((𝑋 ∈ (𝑆𝑧) ∨ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))) ↔ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))))
104 19.43 1883 . . . . . 6 (∃𝑥((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
105 andi 1005 . . . . . . . 8 ((𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
106105bicomi 227 . . . . . . 7 (((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
107106exbii 1849 . . . . . 6 (∃𝑥((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
108104, 107bitr3i 280 . . . . 5 ((∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
109103, 108syl6bb 290 . . . 4 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → ((𝑋 ∈ (𝑆𝑧) ∨ ∃𝑎𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))))
11062eleq2d 2878 . . . . . . . . 9 (𝑧 ∈ ω → (⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧) ↔ ⟨𝑥, ∅⟩ ∈ ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))})))
111 elun 4079 . . . . . . . . . 10 (⟨𝑥, ∅⟩ ∈ ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ ⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}))
112 eqeq1 2805 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣))))
113112rexbidv 3259 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → (∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣))))
114 eqeq1 2805 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝑎 = ∀𝑔𝑖(1st𝑢) ↔ 𝑥 = ∀𝑔𝑖(1st𝑢)))
115114rexbidv 3259 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → (∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))
116113, 115orbi12d 916 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → ((∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)) ↔ (∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))
117116rexbidv 3259 . . . . . . . . . . . . 13 (𝑎 = 𝑥 → (∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)) ↔ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))
11883, 117bi2anan9r 639 . . . . . . . . . . . 12 ((𝑎 = 𝑥𝑏 = ∅) → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))
11942, 43, 118opelopaba 5391 . . . . . . . . . . 11 (⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))} ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))
120119orbi2i 910 . . . . . . . . . 10 ((⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ ⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))
121111, 120bitri 278 . . . . . . . . 9 (⟨𝑥, ∅⟩ ∈ ((𝑆𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑎 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))
122110, 121syl6bb 290 . . . . . . . 8 (𝑧 ∈ ω → (⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))))
123122anbi2d 631 . . . . . . 7 (𝑧 ∈ ω → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))))
124123exbidv 1922 . . . . . 6 (𝑧 ∈ ω → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))))
125124bicomd 226 . . . . 5 (𝑧 ∈ ω → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
126125adantr 484 . . . 4 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆𝑧)(∃𝑣 ∈ (𝑆𝑧)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
12770, 109, 1263bitrd 308 . . 3 ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
128127ex 416 . 2 (𝑧 ∈ ω → ((𝑋 ∈ (𝑆𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑧))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))))
1296, 12, 18, 24, 61, 128finds 7593 1 (𝑁 ∈ ω → (𝑋 ∈ (𝑆𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 844   = wceq 1538  wex 1781  wcel 2112  wrex 3110  cun 3882  c0 4246  cop 4534  {copab 5095  suc csuc 6165  cfv 6328  (class class class)co 7139  ωcom 7564  1st c1st 7673  𝑔cgoe 32694  𝑔cgna 32695  𝑔cgol 32696   Sat csat 32697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-map 8395  df-goel 32701  df-sat 32704
This theorem is referenced by:  fmlasuc  32747
  Copyright terms: Public domain W3C validator