Metamath Proof Explorer

Theorem fmlafvel

Description: A class is a valid Godel formula of height N iff it is the first component of a member of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at N . (Contributed by AV, 19-Sep-2023)

Ref Expression
Assertion fmlafvel ( 𝑁 ∈ ω → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = ∅ → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ ∅ ) )
2 1 eleq2d ⊢ ( 𝑥 = ∅ → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ 𝐹 ∈ ( Fmla ‘ ∅ ) ) )
3 fveq2 ⊢ ( 𝑥 = ∅ → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ ∅ ) )
4 3 eleq2d ⊢ ( 𝑥 = ∅ → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ) )
5 2 4 bibi12d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ↔ ( 𝐹 ∈ ( Fmla ‘ ∅ ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ) ) )
6 5 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ) ↔ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ ∅ ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ) ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑦 → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ 𝑦 ) )
8 7 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ 𝐹 ∈ ( Fmla ‘ 𝑦 ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) )
10 9 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) )
11 8 10 bibi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ) ↔ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) )
13 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ suc 𝑦 ) )
14 13 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ) )
15 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) )
16 15 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) )
17 14 16 bibi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ↔ ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) ) )
18 17 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ) ↔ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) ) ) )
19 fveq2 ⊢ ( 𝑥 = 𝑁 → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ 𝑁 ) )
20 19 eleq2d ⊢ ( 𝑥 = 𝑁 → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ 𝐹 ∈ ( Fmla ‘ 𝑁 ) ) )
21 fveq2 ⊢ ( 𝑥 = 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
22 21 eleq2d ⊢ ( 𝑥 = 𝑁 → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
23 20 22 bibi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑥 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ) ) ↔ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ) )
25 eqeq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) )
26 25 2rexbidv ⊢ ( 𝑥 = 𝐹 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) )
27 26 elrab ⊢ ( 𝐹 ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } ↔ ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) )
28 eqidd ⊢ ( ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) → ∅ = ∅ )
29 simpr ⊢ ( ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) )
30 28 29 jca ⊢ ( ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) → ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) )
31 simpr ⊢ ( ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) )
32 31 anim2i ⊢ ( ( 𝐹 ∈ V ∧ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) → ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) )
33 32 ex ⊢ ( 𝐹 ∈ V → ( ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) → ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
34 30 33 impbid2 ⊢ ( 𝐹 ∈ V → ( ( 𝐹 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
35 27 34 syl5bb ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
36 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
37 36 eleq2i ⊢ ( 𝐹 ∈ ( Fmla ‘ ∅ ) ↔ 𝐹 ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } )
38 37 a1i ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ ∅ ) ↔ 𝐹 ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } ) )
39 satf00 ⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }
40 39 a1i ⊢ ( 𝐹 ∈ V → ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } )
41 40 eleq2d ⊢ ( 𝐹 ∈ V → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) )
42 0ex ⊢ ∅ ∈ V
43 eqeq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 = ∅ ↔ ∅ = ∅ ) )
44 43 26 bi2anan9r ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = ∅ ) → ( ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
45 44 opelopabga ⊢ ( ( 𝐹 ∈ V ∧ ∅ ∈ V ) → ( ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
46 42 45 mpan2 ⊢ ( 𝐹 ∈ V → ( ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
47 41 46 bitrd ⊢ ( 𝐹 ∈ V → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝐹 = ( 𝑖 ∈𝑔 𝑗 ) ) ) )
48 35 38 47 3bitr4d ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ ∅ ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ) )
49 eqid ⊢ ∅ = ∅
50 49 biantrur ⊢ ( ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
51 50 bicomi ⊢ ( ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
52 51 a1i ⊢ ( 𝐹 ∈ V → ( ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
53 eqeq1 ⊢ ( 𝑧 = ∅ → ( 𝑧 = ∅ ↔ ∅ = ∅ ) )
54 eqeq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ↔ 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
55 54 rexbidv ⊢ ( 𝑥 = 𝐹 → ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
56 eqeq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ↔ 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
57 56 rexbidv ⊢ ( 𝑥 = 𝐹 → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ↔ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
58 55 57 orbi12d ⊢ ( 𝑥 = 𝐹 → ( ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
59 58 rexbidv ⊢ ( 𝑥 = 𝐹 → ( ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
60 53 59 bi2anan9r ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑧 = ∅ ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) )
61 60 opelopabga ⊢ ( ( 𝐹 ∈ V ∧ ∅ ∈ V ) → ( ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) )
62 42 61 mpan2 ⊢ ( 𝐹 ∈ V → ( ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) )
63 59 elabg ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝐹 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
64 52 62 63 3bitr4d ⊢ ( 𝐹 ∈ V → ( ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ↔ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) )
65 64 adantl ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ↔ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) )
66 65 orbi2d ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ↔ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ) )
67 eqid ⊢ ( ∅ Sat ∅ ) = ( ∅ Sat ∅ )
68 67 satf0suc ⊢ ( 𝑦 ∈ ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
69 68 eleq2d ⊢ ( 𝑦 ∈ ω → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) )
70 elun ⊢ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ↔ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
71 69 70 bitrdi ⊢ ( 𝑦 ∈ ω → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) )
72 71 ad2antrr ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ⟨ 𝐹 , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) )
73 fmlasuc0 ⊢ ( 𝑦 ∈ ω → ( Fmla ‘ suc 𝑦 ) = ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) )
74 73 eleq2d ⊢ ( 𝑦 ∈ ω → ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ 𝐹 ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ) )
75 74 ad2antrr ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ 𝐹 ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ) )
76 elun ⊢ ( 𝐹 ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ∨ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) )
77 76 a1i ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ∨ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ) )
78 simpr ⊢ ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) → ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) )
79 78 imp ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) )
80 79 orbi1d ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ∨ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ↔ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ) )
81 75 77 80 3bitrd ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ ( ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ 𝐹 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) } ) ) )
82 66 72 81 3bitr4rd ⊢ ( ( ( 𝑦 ∈ ω ∧ ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) ) ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) )
83 82 exp31 ⊢ ( 𝑦 ∈ ω → ( ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) ) → ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ suc 𝑦 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) ) ) )
84 6 12 18 24 48 83 finds ⊢ ( 𝑁 ∈ ω → ( 𝐹 ∈ V → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
85 84 com12 ⊢ ( 𝐹 ∈ V → ( 𝑁 ∈ ω → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
86 prcnel ⊢ ( ¬ 𝐹 ∈ V → ¬ 𝐹 ∈ ( Fmla ‘ 𝑁 ) )
87 86 adantr ⊢ ( ( ¬ 𝐹 ∈ V ∧ 𝑁 ∈ ω ) → ¬ 𝐹 ∈ ( Fmla ‘ 𝑁 ) )
88 opprc1 ⊢ ( ¬ 𝐹 ∈ V → ⟨ 𝐹 , ∅ ⟩ = ∅ )
89 88 adantr ⊢ ( ( ¬ 𝐹 ∈ V ∧ 𝑁 ∈ ω ) → ⟨ 𝐹 , ∅ ⟩ = ∅ )
90 satf0n0 ⊢ ( 𝑁 ∈ ω → ∅ ∉ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
91 df-nel ⊢ ( ∅ ∉ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
92 90 91 sylib ⊢ ( 𝑁 ∈ ω → ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
93 92 adantl ⊢ ( ( ¬ 𝐹 ∈ V ∧ 𝑁 ∈ ω ) → ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
94 89 93 eqneltrd ⊢ ( ( ¬ 𝐹 ∈ V ∧ 𝑁 ∈ ω ) → ¬ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
95 87 94 2falsed ⊢ ( ( ¬ 𝐹 ∈ V ∧ 𝑁 ∈ ω ) → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
96 95 ex ⊢ ( ¬ 𝐹 ∈ V → ( 𝑁 ∈ ω → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
97 85 96 pm2.61i ⊢ ( 𝑁 ∈ ω → ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝐹 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )