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

Theorem fmlasuc 33348
Description: The valid Godel formulas of height (𝑁 + 1), expressed by the valid Godel formulas of height 𝑁. (Contributed by AV, 20-Sep-2023.)
Assertion
Ref Expression
fmlasuc (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
Distinct variable group:   𝑢,𝑁,𝑣,𝑥,𝑖

Proof of Theorem fmlasuc
Dummy variables 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmlasuc0 33346 . 2 (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))}))
2 eqid 2738 . . . . . . . 8 (∅ Sat ∅) = (∅ Sat ∅)
32satf0op 33339 . . . . . . 7 (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat ∅)‘𝑁) ↔ ∃𝑧(𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))))
4 fveq2 6774 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (1st𝑧) = (1st𝑤))
54oveq2d 7291 . . . . . . . . . . 11 (𝑧 = 𝑤 → ((1st𝑦)⊼𝑔(1st𝑧)) = ((1st𝑦)⊼𝑔(1st𝑤)))
65eqeq2d 2749 . . . . . . . . . 10 (𝑧 = 𝑤 → (𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ 𝑥 = ((1st𝑦)⊼𝑔(1st𝑤))))
76cbvrexvw 3384 . . . . . . . . 9 (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ ∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)))
87orbi1i 911 . . . . . . . 8 ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
9 fmlafvel 33347 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ω → (𝑧 ∈ (Fmla‘𝑁) ↔ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
109biimprd 247 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → (⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁) → 𝑧 ∈ (Fmla‘𝑁)))
1110adantld 491 . . . . . . . . . . . . . 14 (𝑁 ∈ ω → ((𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → 𝑧 ∈ (Fmla‘𝑁)))
1211imp 407 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → 𝑧 ∈ (Fmla‘𝑁))
13 vex 3436 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
14 0ex 5231 . . . . . . . . . . . . . . . 16 ∅ ∈ V
1513, 14op1std 7841 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ∅⟩ → (1st𝑦) = 𝑧)
1615eleq1d 2823 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑧, ∅⟩ → ((1st𝑦) ∈ (Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁)))
1716ad2antrl 725 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((1st𝑦) ∈ (Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁)))
1812, 17mpbird 256 . . . . . . . . . . . 12 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (1st𝑦) ∈ (Fmla‘𝑁))
19183adant3 1131 . . . . . . . . . . 11 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) → (1st𝑦) ∈ (Fmla‘𝑁))
20 oveq1 7282 . . . . . . . . . . . . . . 15 (𝑢 = (1st𝑦) → (𝑢𝑔𝑣) = ((1st𝑦)⊼𝑔𝑣))
2120eqeq2d 2749 . . . . . . . . . . . . . 14 (𝑢 = (1st𝑦) → (𝑥 = (𝑢𝑔𝑣) ↔ 𝑥 = ((1st𝑦)⊼𝑔𝑣)))
2221rexbidv 3226 . . . . . . . . . . . . 13 (𝑢 = (1st𝑦) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)))
23 eqidd 2739 . . . . . . . . . . . . . . . 16 (𝑢 = (1st𝑦) → 𝑖 = 𝑖)
24 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (1st𝑦) → 𝑢 = (1st𝑦))
2523, 24goaleq12d 33313 . . . . . . . . . . . . . . 15 (𝑢 = (1st𝑦) → ∀𝑔𝑖𝑢 = ∀𝑔𝑖(1st𝑦))
2625eqeq2d 2749 . . . . . . . . . . . . . 14 (𝑢 = (1st𝑦) → (𝑥 = ∀𝑔𝑖𝑢𝑥 = ∀𝑔𝑖(1st𝑦)))
2726rexbidv 3226 . . . . . . . . . . . . 13 (𝑢 = (1st𝑦) → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
2822, 27orbi12d 916 . . . . . . . . . . . 12 (𝑢 = (1st𝑦) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
2928adantl 482 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) ∧ 𝑢 = (1st𝑦)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
302satf0op 33339 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat ∅)‘𝑁) ↔ ∃𝑦(𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))))
31 fmlafvel 33347 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ω → (𝑦 ∈ (Fmla‘𝑁) ↔ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
3231biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ω → (⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁) → 𝑦 ∈ (Fmla‘𝑁)))
3332adantld 491 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ω → ((𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → 𝑦 ∈ (Fmla‘𝑁)))
3433imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → 𝑦 ∈ (Fmla‘𝑁))
35 vex 3436 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 ∈ V
3635, 14op1std 7841 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑦, ∅⟩ → (1st𝑤) = 𝑦)
3736eleq1d 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ⟨𝑦, ∅⟩ → ((1st𝑤) ∈ (Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁)))
3837ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((1st𝑤) ∈ (Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁)))
3934, 38mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (1st𝑤) ∈ (Fmla‘𝑁))
4039adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) → (1st𝑤) ∈ (Fmla‘𝑁))
41 oveq2 7283 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (1st𝑤) → (𝑧𝑔𝑣) = (𝑧𝑔(1st𝑤)))
4241eqeq2d 2749 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (1st𝑤) → (𝑥 = (𝑧𝑔𝑣) ↔ 𝑥 = (𝑧𝑔(1st𝑤))))
4342adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) ∧ 𝑣 = (1st𝑤)) → (𝑥 = (𝑧𝑔𝑣) ↔ 𝑥 = (𝑧𝑔(1st𝑤))))
44 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) → 𝑥 = (𝑧𝑔(1st𝑤)))
4540, 43, 44rspcedvd 3563 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))
4645exp31 420 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ω → ((𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → (𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
4746exlimdv 1936 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ω → (∃𝑦(𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → (𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
4830, 47sylbid 239 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat ∅)‘𝑁) → (𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
4948rexlimdv 3212 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣)))
5049adantr 481 . . . . . . . . . . . . . 14 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣)))
5115oveq1d 7290 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑧, ∅⟩ → ((1st𝑦)⊼𝑔(1st𝑤)) = (𝑧𝑔(1st𝑤)))
5251eqeq2d 2749 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑧, ∅⟩ → (𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ↔ 𝑥 = (𝑧𝑔(1st𝑤))))
5352rexbidv 3226 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑧, ∅⟩ → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ↔ ∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤))))
5415oveq1d 7290 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑧, ∅⟩ → ((1st𝑦)⊼𝑔𝑣) = (𝑧𝑔𝑣))
5554eqeq2d 2749 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑧, ∅⟩ → (𝑥 = ((1st𝑦)⊼𝑔𝑣) ↔ 𝑥 = (𝑧𝑔𝑣)))
5655rexbidv 3226 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑧, ∅⟩ → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣)))
5753, 56imbi12d 345 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ∅⟩ → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
5857ad2antrl 725 . . . . . . . . . . . . . 14 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
5950, 58mpbird 256 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)))
6059orim1d 963 . . . . . . . . . . . 12 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
61603impia 1116 . . . . . . . . . . 11 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
6219, 29, 61rspcedvd 3563 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
63623exp 1118 . . . . . . . . 9 (𝑁 ∈ ω → ((𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
6463exlimdv 1936 . . . . . . . 8 (𝑁 ∈ ω → (∃𝑧(𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
658, 64syl7bi 254 . . . . . . 7 (𝑁 ∈ ω → (∃𝑧(𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
663, 65sylbid 239 . . . . . 6 (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat ∅)‘𝑁) → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
6766rexlimdv 3212 . . . . 5 (𝑁 ∈ ω → (∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
68 fmlafvel 33347 . . . . . . . . 9 (𝑁 ∈ ω → (𝑢 ∈ (Fmla‘𝑁) ↔ ⟨𝑢, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
6968biimpa 477 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → ⟨𝑢, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
7069adantr 481 . . . . . . 7 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → ⟨𝑢, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
71 vex 3436 . . . . . . . . . . . . 13 𝑢 ∈ V
7271, 14op1std 7841 . . . . . . . . . . . 12 (𝑦 = ⟨𝑢, ∅⟩ → (1st𝑦) = 𝑢)
7372oveq1d 7290 . . . . . . . . . . 11 (𝑦 = ⟨𝑢, ∅⟩ → ((1st𝑦)⊼𝑔(1st𝑧)) = (𝑢𝑔(1st𝑧)))
7473eqeq2d 2749 . . . . . . . . . 10 (𝑦 = ⟨𝑢, ∅⟩ → (𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ 𝑥 = (𝑢𝑔(1st𝑧))))
7574rexbidv 3226 . . . . . . . . 9 (𝑦 = ⟨𝑢, ∅⟩ → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧))))
76 eqidd 2739 . . . . . . . . . . . 12 (𝑦 = ⟨𝑢, ∅⟩ → 𝑖 = 𝑖)
7776, 72goaleq12d 33313 . . . . . . . . . . 11 (𝑦 = ⟨𝑢, ∅⟩ → ∀𝑔𝑖(1st𝑦) = ∀𝑔𝑖𝑢)
7877eqeq2d 2749 . . . . . . . . . 10 (𝑦 = ⟨𝑢, ∅⟩ → (𝑥 = ∀𝑔𝑖(1st𝑦) ↔ 𝑥 = ∀𝑔𝑖𝑢))
7978rexbidv 3226 . . . . . . . . 9 (𝑦 = ⟨𝑢, ∅⟩ → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
8075, 79orbi12d 916 . . . . . . . 8 (𝑦 = ⟨𝑢, ∅⟩ → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
8180adantl 482 . . . . . . 7 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ∧ 𝑦 = ⟨𝑢, ∅⟩) → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
82 fmlafvel 33347 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) ↔ ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
8382biimpd 228 . . . . . . . . . . . . . 14 (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
8483adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (𝑣 ∈ (Fmla‘𝑁) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
8584imp 407 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
8685adantr 481 . . . . . . . . . . 11 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
87 vex 3436 . . . . . . . . . . . . . . 15 𝑣 ∈ V
8887, 14op1std 7841 . . . . . . . . . . . . . 14 (𝑧 = ⟨𝑣, ∅⟩ → (1st𝑧) = 𝑣)
8988oveq2d 7291 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑣, ∅⟩ → (𝑢𝑔(1st𝑧)) = (𝑢𝑔𝑣))
9089eqeq2d 2749 . . . . . . . . . . . 12 (𝑧 = ⟨𝑣, ∅⟩ → (𝑥 = (𝑢𝑔(1st𝑧)) ↔ 𝑥 = (𝑢𝑔𝑣)))
9190adantl 482 . . . . . . . . . . 11 (((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) ∧ 𝑧 = ⟨𝑣, ∅⟩) → (𝑥 = (𝑢𝑔(1st𝑧)) ↔ 𝑥 = (𝑢𝑔𝑣)))
92 simpr 485 . . . . . . . . . . 11 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) → 𝑥 = (𝑢𝑔𝑣))
9386, 91, 92rspcedvd 3563 . . . . . . . . . 10 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)))
9493rexlimdva2 3216 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧))))
9594orim1d 963 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
9695imp 407 . . . . . . 7 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
9770, 81, 96rspcedvd 3563 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
9897rexlimdva2 3216 . . . . 5 (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
9967, 98impbid 211 . . . 4 (𝑁 ∈ ω → (∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
10099abbidv 2807 . . 3 (𝑁 ∈ ω → {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))} = {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})
101100uneq2d 4097 . 2 (𝑁 ∈ ω → ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))}) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
1021, 101eqtrd 2778 1 (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wex 1782  wcel 2106  {cab 2715  wrex 3065  cun 3885  c0 4256  cop 4567  suc csuc 6268  cfv 6433  (class class class)co 7275  ωcom 7712  1st c1st 7829  𝑔cgna 33296  𝑔cgol 33297   Sat csat 33298  Fmlacfmla 33299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-map 8617  df-goel 33302  df-goal 33304  df-sat 33305  df-fmla 33307
This theorem is referenced by:  fmla1  33349  isfmlasuc  33350  fmlasssuc  33351  fmlaomn0  33352
  Copyright terms: Public domain W3C validator