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 32922
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 32920 . 2 (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))}))
2 eqid 2739 . . . . . . . 8 (∅ Sat ∅) = (∅ Sat ∅)
32satf0op 32913 . . . . . . 7 (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat ∅)‘𝑁) ↔ ∃𝑧(𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))))
4 fveq2 6677 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (1st𝑧) = (1st𝑤))
54oveq2d 7189 . . . . . . . . . . 11 (𝑧 = 𝑤 → ((1st𝑦)⊼𝑔(1st𝑧)) = ((1st𝑦)⊼𝑔(1st𝑤)))
65eqeq2d 2750 . . . . . . . . . 10 (𝑧 = 𝑤 → (𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ 𝑥 = ((1st𝑦)⊼𝑔(1st𝑤))))
76cbvrexvw 3351 . . . . . . . . 9 (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ ∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)))
87orbi1i 913 . . . . . . . 8 ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
9 fmlafvel 32921 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ω → (𝑧 ∈ (Fmla‘𝑁) ↔ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
109biimprd 251 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → (⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁) → 𝑧 ∈ (Fmla‘𝑁)))
1110adantld 494 . . . . . . . . . . . . . 14 (𝑁 ∈ ω → ((𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → 𝑧 ∈ (Fmla‘𝑁)))
1211imp 410 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → 𝑧 ∈ (Fmla‘𝑁))
13 vex 3403 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
14 0ex 5176 . . . . . . . . . . . . . . . 16 ∅ ∈ V
1513, 14op1std 7727 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ∅⟩ → (1st𝑦) = 𝑧)
1615eleq1d 2818 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑧, ∅⟩ → ((1st𝑦) ∈ (Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁)))
1716ad2antrl 728 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((1st𝑦) ∈ (Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁)))
1812, 17mpbird 260 . . . . . . . . . . . 12 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (1st𝑦) ∈ (Fmla‘𝑁))
19183adant3 1133 . . . . . . . . . . 11 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) → (1st𝑦) ∈ (Fmla‘𝑁))
20 oveq1 7180 . . . . . . . . . . . . . . 15 (𝑢 = (1st𝑦) → (𝑢𝑔𝑣) = ((1st𝑦)⊼𝑔𝑣))
2120eqeq2d 2750 . . . . . . . . . . . . . 14 (𝑢 = (1st𝑦) → (𝑥 = (𝑢𝑔𝑣) ↔ 𝑥 = ((1st𝑦)⊼𝑔𝑣)))
2221rexbidv 3208 . . . . . . . . . . . . 13 (𝑢 = (1st𝑦) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)))
23 eqidd 2740 . . . . . . . . . . . . . . . 16 (𝑢 = (1st𝑦) → 𝑖 = 𝑖)
24 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (1st𝑦) → 𝑢 = (1st𝑦))
2523, 24goaleq12d 32887 . . . . . . . . . . . . . . 15 (𝑢 = (1st𝑦) → ∀𝑔𝑖𝑢 = ∀𝑔𝑖(1st𝑦))
2625eqeq2d 2750 . . . . . . . . . . . . . 14 (𝑢 = (1st𝑦) → (𝑥 = ∀𝑔𝑖𝑢𝑥 = ∀𝑔𝑖(1st𝑦)))
2726rexbidv 3208 . . . . . . . . . . . . 13 (𝑢 = (1st𝑦) → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
2822, 27orbi12d 918 . . . . . . . . . . . 12 (𝑢 = (1st𝑦) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
2928adantl 485 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) ∧ 𝑢 = (1st𝑦)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
302satf0op 32913 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat ∅)‘𝑁) ↔ ∃𝑦(𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))))
31 fmlafvel 32921 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ω → (𝑦 ∈ (Fmla‘𝑁) ↔ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
3231biimprd 251 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ω → (⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁) → 𝑦 ∈ (Fmla‘𝑁)))
3332adantld 494 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ω → ((𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → 𝑦 ∈ (Fmla‘𝑁)))
3433imp 410 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → 𝑦 ∈ (Fmla‘𝑁))
35 vex 3403 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 ∈ V
3635, 14op1std 7727 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑦, ∅⟩ → (1st𝑤) = 𝑦)
3736eleq1d 2818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ⟨𝑦, ∅⟩ → ((1st𝑤) ∈ (Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁)))
3837ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((1st𝑤) ∈ (Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁)))
3934, 38mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (1st𝑤) ∈ (Fmla‘𝑁))
4039adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) → (1st𝑤) ∈ (Fmla‘𝑁))
41 oveq2 7181 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (1st𝑤) → (𝑧𝑔𝑣) = (𝑧𝑔(1st𝑤)))
4241eqeq2d 2750 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (1st𝑤) → (𝑥 = (𝑧𝑔𝑣) ↔ 𝑥 = (𝑧𝑔(1st𝑤))))
4342adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) ∧ 𝑣 = (1st𝑤)) → (𝑥 = (𝑧𝑔𝑣) ↔ 𝑥 = (𝑧𝑔(1st𝑤))))
44 simpr 488 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) → 𝑥 = (𝑧𝑔(1st𝑤)))
4540, 43, 44rspcedvd 3530 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ω ∧ (𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) ∧ 𝑥 = (𝑧𝑔(1st𝑤))) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))
4645exp31 423 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ω → ((𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → (𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
4746exlimdv 1940 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ω → (∃𝑦(𝑤 = ⟨𝑦, ∅⟩ ∧ ⟨𝑦, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → (𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
4830, 47sylbid 243 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat ∅)‘𝑁) → (𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
4948rexlimdv 3194 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣)))
5049adantr 484 . . . . . . . . . . . . . 14 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣)))
5115oveq1d 7188 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑧, ∅⟩ → ((1st𝑦)⊼𝑔(1st𝑤)) = (𝑧𝑔(1st𝑤)))
5251eqeq2d 2750 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑧, ∅⟩ → (𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ↔ 𝑥 = (𝑧𝑔(1st𝑤))))
5352rexbidv 3208 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑧, ∅⟩ → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ↔ ∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤))))
5415oveq1d 7188 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑧, ∅⟩ → ((1st𝑦)⊼𝑔𝑣) = (𝑧𝑔𝑣))
5554eqeq2d 2750 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑧, ∅⟩ → (𝑥 = ((1st𝑦)⊼𝑔𝑣) ↔ 𝑥 = (𝑧𝑔𝑣)))
5655rexbidv 3208 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑧, ∅⟩ → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣)))
5753, 56imbi12d 348 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ∅⟩ → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
5857ad2antrl 728 . . . . . . . . . . . . . 14 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑧𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧𝑔𝑣))))
5950, 58mpbird 260 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) → ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣)))
6059orim1d 965 . . . . . . . . . . . 12 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
61603impia 1118 . . . . . . . . . . 11 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
6219, 29, 61rspcedvd 3530 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ (𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) ∧ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
63623exp 1120 . . . . . . . . 9 (𝑁 ∈ ω → ((𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
6463exlimdv 1940 . . . . . . . 8 (𝑁 ∈ ω → (∃𝑧(𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → ((∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑤)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
658, 64syl7bi 258 . . . . . . 7 (𝑁 ∈ ω → (∃𝑧(𝑦 = ⟨𝑧, ∅⟩ ∧ ⟨𝑧, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)) → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
663, 65sylbid 243 . . . . . 6 (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat ∅)‘𝑁) → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))))
6766rexlimdv 3194 . . . . 5 (𝑁 ∈ ω → (∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
68 fmlafvel 32921 . . . . . . . . 9 (𝑁 ∈ ω → (𝑢 ∈ (Fmla‘𝑁) ↔ ⟨𝑢, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
6968biimpa 480 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → ⟨𝑢, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
7069adantr 484 . . . . . . 7 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → ⟨𝑢, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
71 vex 3403 . . . . . . . . . . . . 13 𝑢 ∈ V
7271, 14op1std 7727 . . . . . . . . . . . 12 (𝑦 = ⟨𝑢, ∅⟩ → (1st𝑦) = 𝑢)
7372oveq1d 7188 . . . . . . . . . . 11 (𝑦 = ⟨𝑢, ∅⟩ → ((1st𝑦)⊼𝑔(1st𝑧)) = (𝑢𝑔(1st𝑧)))
7473eqeq2d 2750 . . . . . . . . . 10 (𝑦 = ⟨𝑢, ∅⟩ → (𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ 𝑥 = (𝑢𝑔(1st𝑧))))
7574rexbidv 3208 . . . . . . . . 9 (𝑦 = ⟨𝑢, ∅⟩ → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ↔ ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧))))
76 eqidd 2740 . . . . . . . . . . . 12 (𝑦 = ⟨𝑢, ∅⟩ → 𝑖 = 𝑖)
7776, 72goaleq12d 32887 . . . . . . . . . . 11 (𝑦 = ⟨𝑢, ∅⟩ → ∀𝑔𝑖(1st𝑦) = ∀𝑔𝑖𝑢)
7877eqeq2d 2750 . . . . . . . . . 10 (𝑦 = ⟨𝑢, ∅⟩ → (𝑥 = ∀𝑔𝑖(1st𝑦) ↔ 𝑥 = ∀𝑔𝑖𝑢))
7978rexbidv 3208 . . . . . . . . 9 (𝑦 = ⟨𝑢, ∅⟩ → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
8075, 79orbi12d 918 . . . . . . . 8 (𝑦 = ⟨𝑢, ∅⟩ → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
8180adantl 485 . . . . . . 7 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ∧ 𝑦 = ⟨𝑢, ∅⟩) → ((∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
82 fmlafvel 32921 . . . . . . . . . . . . . . 15 (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) ↔ ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
8382biimpd 232 . . . . . . . . . . . . . 14 (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
8483adantr 484 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (𝑣 ∈ (Fmla‘𝑁) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁)))
8584imp 410 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
8685adantr 484 . . . . . . . . . . 11 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) → ⟨𝑣, ∅⟩ ∈ ((∅ Sat ∅)‘𝑁))
87 vex 3403 . . . . . . . . . . . . . . 15 𝑣 ∈ V
8887, 14op1std 7727 . . . . . . . . . . . . . 14 (𝑧 = ⟨𝑣, ∅⟩ → (1st𝑧) = 𝑣)
8988oveq2d 7189 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑣, ∅⟩ → (𝑢𝑔(1st𝑧)) = (𝑢𝑔𝑣))
9089eqeq2d 2750 . . . . . . . . . . . 12 (𝑧 = ⟨𝑣, ∅⟩ → (𝑥 = (𝑢𝑔(1st𝑧)) ↔ 𝑥 = (𝑢𝑔𝑣)))
9190adantl 485 . . . . . . . . . . 11 (((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) ∧ 𝑧 = ⟨𝑣, ∅⟩) → (𝑥 = (𝑢𝑔(1st𝑧)) ↔ 𝑥 = (𝑢𝑔𝑣)))
92 simpr 488 . . . . . . . . . . 11 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) → 𝑥 = (𝑢𝑔𝑣))
9386, 91, 92rspcedvd 3530 . . . . . . . . . 10 ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢𝑔𝑣)) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)))
9493rexlimdva2 3198 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧))))
9594orim1d 965 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
9695imp 410 . . . . . . 7 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
9770, 81, 96rspcedvd 3530 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)))
9897rexlimdva2 3198 . . . . 5 (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))))
9967, 98impbid 215 . . . 4 (𝑁 ∈ ω → (∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦)) ↔ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
10099abbidv 2803 . . 3 (𝑁 ∈ ω → {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))} = {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})
101100uneq2d 4054 . 2 (𝑁 ∈ ω → ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st𝑦)⊼𝑔(1st𝑧)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑦))}) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
1021, 101eqtrd 2774 1 (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 846  w3a 1088   = wceq 1542  wex 1786  wcel 2114  {cab 2717  wrex 3055  cun 3842  c0 4212  cop 4523  suc csuc 6175  cfv 6340  (class class class)co 7173  ωcom 7602  1st c1st 7715  𝑔cgna 32870  𝑔cgol 32871   Sat csat 32872  Fmlacfmla 32873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482  ax-inf2 9180
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-ov 7176  df-oprab 7177  df-mpo 7178  df-om 7603  df-1st 7717  df-2nd 7718  df-wrecs 7979  df-recs 8040  df-rdg 8078  df-map 8442  df-goel 32876  df-goal 32878  df-sat 32879  df-fmla 32881
This theorem is referenced by:  fmla1  32923  isfmlasuc  32924  fmlasssuc  32925  fmlaomn0  32926
  Copyright terms: Public domain W3C validator