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

Theorem sat1el2xp 34898
Description: The first component of an element of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation is a member of a doubled Cartesian product. (Contributed by AV, 17-Sep-2023.)
Assertion
Ref Expression
sat1el2xp (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)))
Distinct variable groups:   𝑤,𝑁   𝑎,𝑏,𝑤
Allowed substitution hints:   𝑁(𝑎,𝑏)

Proof of Theorem sat1el2xp
Dummy variables 𝑥 𝑓 𝑖 𝑗 𝑢 𝑣 𝑟 𝑠 𝑡 𝑦 𝑒 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6885 . . 3 (𝑥 = ∅ → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘∅))
21raleqdv 3319 . 2 (𝑥 = ∅ → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
3 fveq2 6885 . . 3 (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑦))
43raleqdv 3319 . 2 (𝑥 = 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
5 fveq2 6885 . . 3 (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘suc 𝑦))
65raleqdv 3319 . 2 (𝑥 = suc 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
7 fveq2 6885 . . 3 (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑁))
87raleqdv 3319 . 2 (𝑥 = 𝑁 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
9 eqeq1 2730 . . . . . . . 8 (𝑥 = (1st𝑤) → (𝑥 = (𝑖𝑔𝑗) ↔ (1st𝑤) = (𝑖𝑔𝑗)))
1092rexbidv 3213 . . . . . . 7 (𝑥 = (1st𝑤) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗)))
1110anbi2d 628 . . . . . 6 (𝑥 = (1st𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)) ↔ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗))))
12 eqeq1 2730 . . . . . . 7 (𝑧 = (2nd𝑤) → (𝑧 = ∅ ↔ (2nd𝑤) = ∅))
1312anbi1d 629 . . . . . 6 (𝑧 = (2nd𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗)) ↔ ((2nd𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗))))
1411, 13elopabi 8047 . . . . 5 (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))} → ((2nd𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗)))
15 goel 34866 . . . . . . . . 9 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
1615eqeq2d 2737 . . . . . . . 8 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st𝑤) = (𝑖𝑔𝑗) ↔ (1st𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
17 omex 9640 . . . . . . . . . . 11 ω ∈ V
1817, 17pm3.2i 470 . . . . . . . . . 10 (ω ∈ V ∧ ω ∈ V)
19 peano1 7876 . . . . . . . . . . . 12 ∅ ∈ ω
2019a1i 11 . . . . . . . . . . 11 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ∈ ω)
21 opelxpi 5706 . . . . . . . . . . 11 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨𝑖, 𝑗⟩ ∈ (ω × ω))
2220, 21opelxpd 5708 . . . . . . . . . 10 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)))
23 xpeq12 5694 . . . . . . . . . . . . 13 ((𝑎 = ω ∧ 𝑏 = ω) → (𝑎 × 𝑏) = (ω × ω))
2423xpeq2d 5699 . . . . . . . . . . . 12 ((𝑎 = ω ∧ 𝑏 = ω) → (ω × (𝑎 × 𝑏)) = (ω × (ω × ω)))
2524eleq2d 2813 . . . . . . . . . . 11 ((𝑎 = ω ∧ 𝑏 = ω) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω))))
2625spc2egv 3583 . . . . . . . . . 10 ((ω ∈ V ∧ ω ∈ V) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)) → ∃𝑎𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
2718, 22, 26mpsyl 68 . . . . . . . . 9 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∃𝑎𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)))
28 eleq1 2815 . . . . . . . . . 10 ((1st𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → ((1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
29282exbidv 1919 . . . . . . . . 9 ((1st𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → (∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
3027, 29syl5ibrcom 246 . . . . . . . 8 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → ∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
3116, 30sylbid 239 . . . . . . 7 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st𝑤) = (𝑖𝑔𝑗) → ∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
3231rexlimivv 3193 . . . . . 6 (∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗) → ∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)))
3332adantl 481 . . . . 5 (((2nd𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st𝑤) = (𝑖𝑔𝑗)) → ∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)))
3414, 33syl 17 . . . 4 (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))} → ∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)))
35 satf00 34893 . . . 4 ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))}
3634, 35eleq2s 2845 . . 3 (𝑤 ∈ ((∅ Sat ∅)‘∅) → ∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)))
3736rgen 3057 . 2 𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))
38 omsucelsucb 8459 . . . . . . . . . . 11 (𝑦 ∈ ω ↔ suc 𝑦 ∈ suc ω)
39 satf0sucom 34892 . . . . . . . . . . 11 (suc 𝑦 ∈ suc ω → ((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦))
4038, 39sylbi 216 . . . . . . . . . 10 (𝑦 ∈ ω → ((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦))
4140adantr 480 . . . . . . . . 9 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦))
42 nnon 7858 . . . . . . . . . . . 12 (𝑦 ∈ ω → 𝑦 ∈ On)
43 rdgsuc 8425 . . . . . . . . . . . 12 (𝑦 ∈ On → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦)))
4442, 43syl 17 . . . . . . . . . . 11 (𝑦 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦)))
4544adantr 480 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦)))
46 elelsuc 6431 . . . . . . . . . . . . . 14 (𝑦 ∈ ω → 𝑦 ∈ suc ω)
47 satf0sucom 34892 . . . . . . . . . . . . . 14 (𝑦 ∈ suc ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦))
4846, 47syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦))
4948eqcomd 2732 . . . . . . . . . . . 12 (𝑦 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦) = ((∅ Sat ∅)‘𝑦))
5049fveq2d 6889 . . . . . . . . . . 11 (𝑦 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘((∅ Sat ∅)‘𝑦)))
5150adantr 480 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘𝑦)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘((∅ Sat ∅)‘𝑦)))
52 eqidd 2727 . . . . . . . . . . 11 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})))
53 id 22 . . . . . . . . . . . . 13 (𝑓 = ((∅ Sat ∅)‘𝑦) → 𝑓 = ((∅ Sat ∅)‘𝑦))
54 rexeq 3315 . . . . . . . . . . . . . . . . 17 (𝑓 = ((∅ Sat ∅)‘𝑦) → (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣))))
5554orbi1d 913 . . . . . . . . . . . . . . . 16 (𝑓 = ((∅ Sat ∅)‘𝑦) → ((∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))
5655rexeqbi1dv 3328 . . . . . . . . . . . . . . 15 (𝑓 = ((∅ Sat ∅)‘𝑦) → (∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))))
5756anbi2d 628 . . . . . . . . . . . . . 14 (𝑓 = ((∅ Sat ∅)‘𝑦) → ((𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))) ↔ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))))
5857opabbidv 5207 . . . . . . . . . . . . 13 (𝑓 = ((∅ Sat ∅)‘𝑦) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))} = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})
5953, 58uneq12d 4159 . . . . . . . . . . . 12 (𝑓 = ((∅ Sat ∅)‘𝑦) → (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))
6059adantl 481 . . . . . . . . . . 11 (((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) ∧ 𝑓 = ((∅ Sat ∅)‘𝑦)) → (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))
61 fvexd 6900 . . . . . . . . . . 11 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘𝑦) ∈ V)
6217a1i 11 . . . . . . . . . . . . 13 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ω ∈ V)
63 satf0suclem 34894 . . . . . . . . . . . . 13 ((((∅ Sat ∅)‘𝑦) ∈ V ∧ ((∅ Sat ∅)‘𝑦) ∈ V ∧ ω ∈ V) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))} ∈ V)
6461, 61, 62, 63syl3anc 1368 . . . . . . . . . . . 12 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))} ∈ V)
65 unexg 7733 . . . . . . . . . . . 12 ((((∅ Sat ∅)‘𝑦) ∈ V ∧ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))} ∈ V) → (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}) ∈ V)
6661, 64, 65syl2anc 583 . . . . . . . . . . 11 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}) ∈ V)
6752, 60, 61, 66fvmptd 6999 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))‘((∅ Sat ∅)‘𝑦)) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))
6845, 51, 673eqtrd 2770 . . . . . . . . 9 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢𝑓 (∃𝑣𝑓 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗))})‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))
6941, 68eqtrd 2766 . . . . . . . 8 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))
7069eleq2d 2813 . . . . . . 7 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) ↔ 𝑡 ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})))
71 elun 4143 . . . . . . 7 (𝑡 ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}) ↔ (𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}))
7270, 71bitrdi 287 . . . . . 6 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) ↔ (𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))})))
73 fveq2 6885 . . . . . . . . . . 11 (𝑤 = 𝑡 → (1st𝑤) = (1st𝑡))
7473eleq1d 2812 . . . . . . . . . 10 (𝑤 = 𝑡 → ((1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
75742exbidv 1919 . . . . . . . . 9 (𝑤 = 𝑡 → (∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
7675rspccv 3603 . . . . . . . 8 (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
7776adantl 481 . . . . . . 7 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
78 fveq2 6885 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑣 → (1st𝑤) = (1st𝑣))
7978eleq1d 2812 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑣 → ((1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st𝑣) ∈ (ω × (𝑎 × 𝑏))))
80792exbidv 1919 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑣 → (∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎𝑏(1st𝑣) ∈ (ω × (𝑎 × 𝑏))))
8180rspcva 3604 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑣) ∈ (ω × (𝑎 × 𝑏)))
82 sels 5431 . . . . . . . . . . . . . . . . . 18 ((1st𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st𝑣) ∈ 𝑠)
8382exlimivv 1927 . . . . . . . . . . . . . . . . 17 (∃𝑎𝑏(1st𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st𝑣) ∈ 𝑠)
8481, 83syl 17 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st𝑣) ∈ 𝑠)
8584expcom 413 . . . . . . . . . . . . . . 15 (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑠(1st𝑣) ∈ 𝑠))
86 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑢 → (1st𝑤) = (1st𝑢))
8786eleq1d 2812 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑢 → ((1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st𝑢) ∈ (ω × (𝑎 × 𝑏))))
88872exbidv 1919 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑢 → (∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎𝑏(1st𝑢) ∈ (ω × (𝑎 × 𝑏))))
8988rspcva 3604 . . . . . . . . . . . . . . . . . . 19 ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑢) ∈ (ω × (𝑎 × 𝑏)))
90 sels 5431 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st𝑢) ∈ 𝑠)
9190exlimivv 1927 . . . . . . . . . . . . . . . . . . 19 (∃𝑎𝑏(1st𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st𝑢) ∈ 𝑠)
9289, 91syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st𝑢) ∈ 𝑠)
93 eleq2w 2811 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑟 → ((1st𝑢) ∈ 𝑠 ↔ (1st𝑢) ∈ 𝑟))
9493cbvexvw 2032 . . . . . . . . . . . . . . . . . . 19 (∃𝑠(1st𝑢) ∈ 𝑠 ↔ ∃𝑟(1st𝑢) ∈ 𝑟)
95 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟 ∈ V
96 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑠 ∈ V
9795, 96pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 ∈ V ∧ 𝑠 ∈ V)
98 df-ov 7408 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1st𝑢)⊼𝑔(1st𝑣)) = (⊼𝑔‘⟨(1st𝑢), (1st𝑣)⟩)
99 df-gona 34860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑔 = (𝑒 ∈ (V × V) ↦ ⟨1o, 𝑒⟩)
100 opeq2 4869 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 = ⟨(1st𝑢), (1st𝑣)⟩ → ⟨1o, 𝑒⟩ = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
101 opelvvg 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ⟨(1st𝑢), (1st𝑣)⟩ ∈ (V × V))
102 opex 5457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ ∈ V
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ ∈ V)
10499, 100, 101, 103fvmptd3 7015 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → (⊼𝑔‘⟨(1st𝑢), (1st𝑣)⟩) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
10598, 104eqtrid 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
106 1onn 8641 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1o ∈ ω
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → 1o ∈ ω)
108 opelxpi 5706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ⟨(1st𝑢), (1st𝑣)⟩ ∈ (𝑟 × 𝑠))
109107, 108opelxpd 5708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ ∈ (ω × (𝑟 × 𝑠)))
110105, 109eqeltrd 2827 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑟 × 𝑠)))
111 xpeq12 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 = 𝑟𝑏 = 𝑠) → (𝑎 × 𝑏) = (𝑟 × 𝑠))
112111xpeq2d 5699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑟𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (𝑟 × 𝑠)))
113112eleq2d 2813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑟𝑏 = 𝑠) → (((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑟 × 𝑠))))
114113spc2egv 3583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑟 ∈ V ∧ 𝑠 ∈ V) → (((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑟 × 𝑠)) → ∃𝑎𝑏((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑎 × 𝑏))))
11597, 110, 114mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ∃𝑎𝑏((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑎 × 𝑏)))
116 eleq1 2815 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → ((1st𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑎 × 𝑏))))
1171162exbidv 1919 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎𝑏((1st𝑢)⊼𝑔(1st𝑣)) ∈ (ω × (𝑎 × 𝑏))))
118115, 117syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) ∈ 𝑟 ∧ (1st𝑣) ∈ 𝑠) → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
119118ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝑢) ∈ 𝑟 → ((1st𝑣) ∈ 𝑠 → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
120119exlimdv 1928 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑢) ∈ 𝑟 → (∃𝑠(1st𝑣) ∈ 𝑠 → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
121120com23 86 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑢) ∈ 𝑟 → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (∃𝑠(1st𝑣) ∈ 𝑠 → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
122121exlimiv 1925 . . . . . . . . . . . . . . . . . . 19 (∃𝑟(1st𝑢) ∈ 𝑟 → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (∃𝑠(1st𝑣) ∈ 𝑠 → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
12394, 122sylbi 216 . . . . . . . . . . . . . . . . . 18 (∃𝑠(1st𝑢) ∈ 𝑠 → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (∃𝑠(1st𝑣) ∈ 𝑠 → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
12492, 123syl 17 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (∃𝑠(1st𝑣) ∈ 𝑠 → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
125124expcom 413 . . . . . . . . . . . . . . . 16 (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (∃𝑠(1st𝑣) ∈ 𝑠 → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
126125com24 95 . . . . . . . . . . . . . . 15 (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (∃𝑠(1st𝑣) ∈ 𝑠 → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
12785, 126syld 47 . . . . . . . . . . . . . 14 (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
128127adantl 481 . . . . . . . . . . . . 13 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
129128com14 96 . . . . . . . . . . . 12 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ((1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
130129rexlimdv 3147 . . . . . . . . . . 11 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
13117, 96pm3.2i 470 . . . . . . . . . . . . . . . . . . . . 21 (ω ∈ V ∧ 𝑠 ∈ V)
132 df-goal 34861 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔𝑖(1st𝑢) = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩
133 2onn 8643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2o ∈ ω
134133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω) → 2o ∈ ω)
135 opelxpi 5706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ω ∧ (1st𝑢) ∈ 𝑠) → ⟨𝑖, (1st𝑢)⟩ ∈ (ω × 𝑠))
136135ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω) → ⟨𝑖, (1st𝑢)⟩ ∈ (ω × 𝑠))
137134, 136opelxpd 5708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω) → ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ ∈ (ω × (ω × 𝑠)))
138132, 137eqeltrid 2831 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω) → ∀𝑔𝑖(1st𝑢) ∈ (ω × (ω × 𝑠)))
1391383adant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω ∧ (1st𝑡) = ∀𝑔𝑖(1st𝑢)) → ∀𝑔𝑖(1st𝑢) ∈ (ω × (ω × 𝑠)))
140 eleq1 2815 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → ((1st𝑡) ∈ (ω × (ω × 𝑠)) ↔ ∀𝑔𝑖(1st𝑢) ∈ (ω × (ω × 𝑠))))
1411403ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω ∧ (1st𝑡) = ∀𝑔𝑖(1st𝑢)) → ((1st𝑡) ∈ (ω × (ω × 𝑠)) ↔ ∀𝑔𝑖(1st𝑢) ∈ (ω × (ω × 𝑠))))
142139, 141mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω ∧ (1st𝑡) = ∀𝑔𝑖(1st𝑢)) → (1st𝑡) ∈ (ω × (ω × 𝑠)))
143 xpeq12 5694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 = ω ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (ω × 𝑠))
144143xpeq2d 5699 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 = ω ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (ω × 𝑠)))
145144eleq2d 2813 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = ω ∧ 𝑏 = 𝑠) → ((1st𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st𝑡) ∈ (ω × (ω × 𝑠))))
146145spc2egv 3583 . . . . . . . . . . . . . . . . . . . . 21 ((ω ∈ V ∧ 𝑠 ∈ V) → ((1st𝑡) ∈ (ω × (ω × 𝑠)) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
147131, 142, 146mpsyl 68 . . . . . . . . . . . . . . . . . . . 20 (((1st𝑢) ∈ 𝑠𝑖 ∈ ω ∧ (1st𝑡) = ∀𝑔𝑖(1st𝑢)) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))
1481473exp 1116 . . . . . . . . . . . . . . . . . . 19 ((1st𝑢) ∈ 𝑠 → (𝑖 ∈ ω → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
149148com23 86 . . . . . . . . . . . . . . . . . 18 ((1st𝑢) ∈ 𝑠 → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → (𝑖 ∈ ω → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
150149a1d 25 . . . . . . . . . . . . . . . . 17 ((1st𝑢) ∈ 𝑠 → (𝑦 ∈ ω → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → (𝑖 ∈ ω → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
151150exlimiv 1925 . . . . . . . . . . . . . . . 16 (∃𝑠(1st𝑢) ∈ 𝑠 → (𝑦 ∈ ω → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → (𝑖 ∈ ω → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
15292, 151syl 17 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑦 ∈ ω → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → (𝑖 ∈ ω → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
153152ex 412 . . . . . . . . . . . . . 14 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑦 ∈ ω → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → (𝑖 ∈ ω → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))))
154153impcomd 411 . . . . . . . . . . . . 13 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → (𝑖 ∈ ω → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
155154com24 95 . . . . . . . . . . . 12 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (𝑖 ∈ ω → ((1st𝑡) = ∀𝑔𝑖(1st𝑢) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))))
156155rexlimdv 3147 . . . . . . . . . . 11 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
157130, 156jaod 856 . . . . . . . . . 10 (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ((∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
158157rexlimiv 3142 . . . . . . . . 9 (∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
159158adantl 481 . . . . . . . 8 (((2nd𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢))) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
160 eqeq1 2730 . . . . . . . . . . . . 13 (𝑥 = (1st𝑡) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ (1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣))))
161160rexbidv 3172 . . . . . . . . . . . 12 (𝑥 = (1st𝑡) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣))))
162 eqeq1 2730 . . . . . . . . . . . . 13 (𝑥 = (1st𝑡) → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ (1st𝑡) = ∀𝑔𝑖(1st𝑢)))
163162rexbidv 3172 . . . . . . . . . . . 12 (𝑥 = (1st𝑡) → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢) ↔ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢)))
164161, 163orbi12d 915 . . . . . . . . . . 11 (𝑥 = (1st𝑡) → ((∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢))))
165164rexbidv 3172 . . . . . . . . . 10 (𝑥 = (1st𝑡) → (∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢))))
166165anbi2d 628 . . . . . . . . 9 (𝑥 = (1st𝑡) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢))) ↔ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢)))))
167 eqeq1 2730 . . . . . . . . . 10 (𝑧 = (2nd𝑡) → (𝑧 = ∅ ↔ (2nd𝑡) = ∅))
168167anbi1d 629 . . . . . . . . 9 (𝑧 = (2nd𝑡) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢))) ↔ ((2nd𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢)))))
169166, 168elopabi 8047 . . . . . . . 8 (𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))} → ((2nd𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st𝑡) = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω (1st𝑡) = ∀𝑔𝑖(1st𝑢))))
170159, 169syl11 33 . . . . . . 7 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))} → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
17177, 170jaod 856 . . . . . 6 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)))}) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
17272, 171sylbid 239 . . . . 5 ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
173172ex 412 . . . 4 (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) → ∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))))
174173ralrimdv 3146 . . 3 (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏))))
17575cbvralvw 3228 . . 3 (∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎𝑏(1st𝑡) ∈ (ω × (𝑎 × 𝑏)))
176174, 175imbitrrdi 251 . 2 (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏))))
1772, 4, 6, 8, 37, 176finds 7886 1 (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎𝑏(1st𝑤) ∈ (ω × (𝑎 × 𝑏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 844  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wral 3055  wrex 3064  Vcvv 3468  cun 3941  c0 4317  cop 4629  {copab 5203  cmpt 5224   × cxp 5667  Oncon0 6358  suc csuc 6360  cfv 6537  (class class class)co 7405  ωcom 7852  1st c1st 7972  2nd c2nd 7973  reccrdg 8410  1oc1o 8460  2oc2o 8461  𝑔cgoe 34852  𝑔cgna 34853  𝑔cgol 34854   Sat csat 34855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-map 8824  df-goel 34859  df-gona 34860  df-goal 34861  df-sat 34862
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator