Metamath Proof Explorer


Theorem fmlasuc

Description: The valid Godel formulas of height ( N + 1 ) , expressed by the valid Godel formulas of height N . (Contributed by AV, 20-Sep-2023)

Ref Expression
Assertion fmlasuc ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) )

Proof

Step Hyp Ref Expression
1 fmlasuc0 ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) } ) )
2 eqid ( ∅ Sat ∅ ) = ( ∅ Sat ∅ )
3 2 satf0op ( 𝑁 ∈ ω → ( 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
4 fveq2 ( 𝑧 = 𝑤 → ( 1st𝑧 ) = ( 1st𝑤 ) )
5 4 oveq2d ( 𝑧 = 𝑤 → ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) )
6 5 eqeq2d ( 𝑧 = 𝑤 → ( 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ↔ 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ) )
7 6 cbvrexvw ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ↔ ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) )
8 7 orbi1i ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) )
9 fmlafvel ( 𝑁 ∈ ω → ( 𝑧 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
10 9 biimprd ( 𝑁 ∈ ω → ( ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
11 10 adantld ( 𝑁 ∈ ω → ( ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
12 11 imp ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) )
13 vex 𝑧 ∈ V
14 0ex ∅ ∈ V
15 13 14 op1std ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( 1st𝑦 ) = 𝑧 )
16 15 eleq1d ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( 1st𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
17 16 ad2antrl ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( 1st𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
18 12 17 mpbird ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( 1st𝑦 ) ∈ ( Fmla ‘ 𝑁 ) )
19 18 3adant3 ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) → ( 1st𝑦 ) ∈ ( Fmla ‘ 𝑁 ) )
20 oveq1 ( 𝑢 = ( 1st𝑦 ) → ( 𝑢𝑔 𝑣 ) = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) )
21 20 eqeq2d ( 𝑢 = ( 1st𝑦 ) → ( 𝑥 = ( 𝑢𝑔 𝑣 ) ↔ 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ) )
22 21 rexbidv ( 𝑢 = ( 1st𝑦 ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ) )
23 eqidd ( 𝑢 = ( 1st𝑦 ) → 𝑖 = 𝑖 )
24 id ( 𝑢 = ( 1st𝑦 ) → 𝑢 = ( 1st𝑦 ) )
25 23 24 goaleq12d ( 𝑢 = ( 1st𝑦 ) → ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑖 ( 1st𝑦 ) )
26 25 eqeq2d ( 𝑢 = ( 1st𝑦 ) → ( 𝑥 = ∀𝑔 𝑖 𝑢𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) )
27 26 rexbidv ( 𝑢 = ( 1st𝑦 ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) )
28 22 27 orbi12d ( 𝑢 = ( 1st𝑦 ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) )
29 28 adantl ( ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) ∧ 𝑢 = ( 1st𝑦 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) )
30 2 satf0op ( 𝑁 ∈ ω → ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
31 fmlafvel ( 𝑁 ∈ ω → ( 𝑦 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
32 31 biimprd ( 𝑁 ∈ ω → ( ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
33 32 adantld ( 𝑁 ∈ ω → ( ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
34 33 imp ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) )
35 vex 𝑦 ∈ V
36 35 14 op1std ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ → ( 1st𝑤 ) = 𝑦 )
37 36 eleq1d ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ → ( ( 1st𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
38 37 ad2antrl ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( 1st𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
39 34 38 mpbird ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( 1st𝑤 ) ∈ ( Fmla ‘ 𝑁 ) )
40 39 adantr ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) → ( 1st𝑤 ) ∈ ( Fmla ‘ 𝑁 ) )
41 oveq2 ( 𝑣 = ( 1st𝑤 ) → ( 𝑧𝑔 𝑣 ) = ( 𝑧𝑔 ( 1st𝑤 ) ) )
42 41 eqeq2d ( 𝑣 = ( 1st𝑤 ) → ( 𝑥 = ( 𝑧𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) )
43 42 adantl ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) ∧ 𝑣 = ( 1st𝑤 ) ) → ( 𝑥 = ( 𝑧𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) )
44 simpr ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) → 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) )
45 40 43 44 rspcedvd ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) )
46 45 exp31 ( 𝑁 ∈ ω → ( ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) ) )
47 46 exlimdv ( 𝑁 ∈ ω → ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) ) )
48 30 47 sylbid ( 𝑁 ∈ ω → ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) ) )
49 48 rexlimdv ( 𝑁 ∈ ω → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) )
50 49 adantr ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) )
51 15 oveq1d ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) = ( 𝑧𝑔 ( 1st𝑤 ) ) )
52 51 eqeq2d ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ↔ 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) )
53 52 rexbidv ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ↔ ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) ) )
54 15 oveq1d ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) = ( 𝑧𝑔 𝑣 ) )
55 54 eqeq2d ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧𝑔 𝑣 ) ) )
56 55 rexbidv ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) )
57 53 56 imbi12d ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) ) )
58 57 ad2antrl ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧𝑔 𝑣 ) ) ) )
59 50 58 mpbird ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ) )
60 59 orim1d ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) )
61 60 3impia ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) )
62 19 29 61 rspcedvd ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
63 62 3exp ( 𝑁 ∈ ω → ( ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) )
64 63 exlimdv ( 𝑁 ∈ ω → ( ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) )
65 8 64 syl7bi ( 𝑁 ∈ ω → ( ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) )
66 3 65 sylbid ( 𝑁 ∈ ω → ( 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) )
67 66 rexlimdv ( 𝑁 ∈ ω → ( ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
68 fmlafvel ( 𝑁 ∈ ω → ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑢 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
69 68 biimpa ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ⟨ 𝑢 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
70 69 adantr ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) → ⟨ 𝑢 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
71 vex 𝑢 ∈ V
72 71 14 op1std ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( 1st𝑦 ) = 𝑢 )
73 72 oveq1d ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) = ( 𝑢𝑔 ( 1st𝑧 ) ) )
74 73 eqeq2d ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ↔ 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ) )
75 74 rexbidv ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ↔ ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ) )
76 eqidd ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → 𝑖 = 𝑖 )
77 76 72 goaleq12d ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ∀𝑔 𝑖 ( 1st𝑦 ) = ∀𝑔 𝑖 𝑢 )
78 77 eqeq2d ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ↔ 𝑥 = ∀𝑔 𝑖 𝑢 ) )
79 78 rexbidv ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
80 75 79 orbi12d ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ↔ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
81 80 adantl ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ∧ 𝑦 = ⟨ 𝑢 , ∅ ⟩ ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ↔ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
82 fmlafvel ( 𝑁 ∈ ω → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
83 82 biimpd ( 𝑁 ∈ ω → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
84 83 adantr ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
85 84 imp ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
86 85 adantr ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢𝑔 𝑣 ) ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
87 vex 𝑣 ∈ V
88 87 14 op1std ( 𝑧 = ⟨ 𝑣 , ∅ ⟩ → ( 1st𝑧 ) = 𝑣 )
89 88 oveq2d ( 𝑧 = ⟨ 𝑣 , ∅ ⟩ → ( 𝑢𝑔 ( 1st𝑧 ) ) = ( 𝑢𝑔 𝑣 ) )
90 89 eqeq2d ( 𝑧 = ⟨ 𝑣 , ∅ ⟩ → ( 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ↔ 𝑥 = ( 𝑢𝑔 𝑣 ) ) )
91 90 adantl ( ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢𝑔 𝑣 ) ) ∧ 𝑧 = ⟨ 𝑣 , ∅ ⟩ ) → ( 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ↔ 𝑥 = ( 𝑢𝑔 𝑣 ) ) )
92 simpr ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢𝑔 𝑣 ) ) → 𝑥 = ( 𝑢𝑔 𝑣 ) )
93 86 91 92 rspcedvd ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢𝑔 𝑣 ) ) → ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) )
94 93 rexlimdva2 ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) → ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ) )
95 94 orim1d ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
96 95 imp ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
97 70 81 96 rspcedvd ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) → ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) )
98 97 rexlimdva2 ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) → ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ) )
99 67 98 impbid ( 𝑁 ∈ ω → ( ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
100 99 abbidv ( 𝑁 ∈ ω → { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } )
101 100 uneq2d ( 𝑁 ∈ ω → ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st𝑦 ) ⊼𝑔 ( 1st𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑦 ) ) } ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) )
102 1 101 eqtrd ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) )