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