This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmlasucdisj

Description: The valid Godel formulas of height ( N + 1 ) is disjoint with the difference ( ( Fmlasuc suc N ) \ ( Fmlasuc N ) ) , expressed by formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification based on the valid Godel formulas of height ( N + 1 ) . (Contributed by AV, 20-Oct-2023)

Ref Expression
Assertion fmlasucdisj ( 𝑁 ∈ ω → ( ( Fmla ‘ suc 𝑁 ) ∩ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } ) = ∅ )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑓 ∈ V
2 eqeq1 ⊢ ( 𝑥 = 𝑓 → ( 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
3 2 rexbidv ⊢ ( 𝑥 = 𝑓 → ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
4 eqeq1 ⊢ ( 𝑥 = 𝑓 → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ 𝑓 = ∀𝑔 𝑖 𝑢 ) )
5 4 rexbidv ⊢ ( 𝑥 = 𝑓 → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) )
6 3 5 orbi12d ⊢ ( 𝑥 = 𝑓 → ( ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ) )
7 6 rexbidv ⊢ ( 𝑥 = 𝑓 → ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ) )
8 2 2rexbidv ⊢ ( 𝑥 = 𝑓 → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
9 7 8 orbi12d ⊢ ( 𝑥 = 𝑓 → ( ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) ↔ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) )
10 1 9 elab ⊢ ( 𝑓 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } ↔ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
11 gonar ⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) )
12 elndif ⊢ ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) → ¬ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
13 12 adantr ⊢ ( ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
14 13 intnanrd ⊢ ( ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) )
15 11 14 syl ⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) )
16 15 ex ⊢ ( 𝑁 ∈ ω → ( ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) → ¬ ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) ) )
17 16 con2d ⊢ ( 𝑁 ∈ ω → ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) )
18 17 impl ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) )
19 elneeldif ⊢ ( ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → 𝑎 ≠ 𝑢 )
20 19 necomd ⊢ ( ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → 𝑢 ≠ 𝑎 )
21 20 ancoms ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑢 ≠ 𝑎 )
22 21 neneqd ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ 𝑢 = 𝑎 )
23 22 orcd ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ( ¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏 ) )
24 ianor ⊢ ( ¬ ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ↔ ( ¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏 ) )
25 vex ⊢ 𝑢 ∈ V
26 vex ⊢ 𝑣 ∈ V
27 25 26 opth ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) )
28 24 27 xchnxbir ⊢ ( ¬ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ( ¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏 ) )
29 23 28 sylibr ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
30 29 olcd ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ( ¬ 1o = 1o ∨ ¬ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
31 ianor ⊢ ( ¬ ( 1o = 1o ∧ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( ¬ 1o = 1o ∨ ¬ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
32 gonafv ⊢ ( ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑢 ⊼𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
33 32 el2v ⊢ ( 𝑢 ⊼𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩
34 gonafv ⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 ⊼𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
35 34 el2v ⊢ ( 𝑎 ⊼𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩
36 33 35 eqeq12i ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
37 1oex ⊢ 1o ∈ V
38 opex ⊢ ⟨ 𝑢 , 𝑣 ⟩ ∈ V
39 37 38 opth ⊢ ( ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ ↔ ( 1o = 1o ∧ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
40 36 39 bitri ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ( 1o = 1o ∧ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
41 31 40 xchnxbir ⊢ ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ( ¬ 1o = 1o ∨ ¬ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
42 30 41 sylibr ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
43 42 ralrimivw ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
44 43 ralrimiva ⊢ ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
45 44 adantl ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
46 45 adantr ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
47 gonanegoal ⊢ ( 𝑢 ⊼𝑔 𝑣 ) ≠ ∀𝑔 𝑗 𝑎
48 47 neii ⊢ ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎
49 48 a1i ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 )
50 49 ralrimivw ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 )
51 50 ralrimivw ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 )
52 r19.26 ⊢ ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ↔ ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) )
53 46 51 52 sylanbrc ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) )
54 18 53 jca ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) )
55 eleq1 ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ↔ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) )
56 55 notbid ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ↔ ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) )
57 eqeq1 ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ) )
58 57 notbid ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ) )
59 58 ralbidv ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ) )
60 eqeq1 ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( 𝑓 = ∀𝑔 𝑗 𝑎 ↔ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) )
61 60 notbid ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ↔ ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) )
62 61 ralbidv ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ↔ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) )
63 59 62 anbi12d ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) )
64 63 ralbidv ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) )
65 56 64 anbi12d ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) ) )
66 54 65 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
67 66 rexlimdva ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
68 goalr ⊢ ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑢 ∈ ( Fmla ‘ 𝑁 ) )
69 68 12 syl ⊢ ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
70 69 ex ⊢ ( 𝑁 ∈ ω → ( ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) → ¬ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) )
71 70 con2d ⊢ ( 𝑁 ∈ ω → ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) )
72 71 imp ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) )
73 72 adantr ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) )
74 gonanegoal ⊢ ( 𝑎 ⊼𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢
75 74 nesymi ⊢ ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 )
76 75 a1i ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) )
77 76 ralrimivw ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) )
78 77 ralrimivw ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) )
79 22 olcd ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ( ¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎 ) )
80 ianor ⊢ ( ¬ ( 𝑖 = 𝑗 ∧ 𝑢 = 𝑎 ) ↔ ( ¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎 ) )
81 vex ⊢ 𝑖 ∈ V
82 81 25 opth ⊢ ( ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ↔ ( 𝑖 = 𝑗 ∧ 𝑢 = 𝑎 ) )
83 80 82 xchnxbir ⊢ ( ¬ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ↔ ( ¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎 ) )
84 79 83 sylibr ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ )
85 84 olcd ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ( ¬ 2o = 2o ∨ ¬ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ) )
86 ianor ⊢ ( ¬ ( 2o = 2o ∧ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ) ↔ ( ¬ 2o = 2o ∨ ¬ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ) )
87 2oex ⊢ 2o ∈ V
88 opex ⊢ ⟨ 𝑖 , 𝑢 ⟩ ∈ V
89 87 88 opth ⊢ ( ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑗 , 𝑎 ⟩ ⟩ ↔ ( 2o = 2o ∧ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ) )
90 86 89 xchnxbir ⊢ ( ¬ ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑗 , 𝑎 ⟩ ⟩ ↔ ( ¬ 2o = 2o ∨ ¬ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ) )
91 df-goal ⊢ ∀𝑔 𝑖 𝑢 = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩
92 df-goal ⊢ ∀𝑔 𝑗 𝑎 = ⟨ 2o , ⟨ 𝑗 , 𝑎 ⟩ ⟩
93 91 92 eqeq12i ⊢ ( ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ↔ ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑗 , 𝑎 ⟩ ⟩ )
94 90 93 xchnxbir ⊢ ( ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ↔ ( ¬ 2o = 2o ∨ ¬ ⟨ 𝑖 , 𝑢 ⟩ = ⟨ 𝑗 , 𝑎 ⟩ ) )
95 85 94 sylibr ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 )
96 95 ralrimivw ⊢ ( ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 )
97 96 ralrimiva ⊢ ( 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 )
98 97 adantl ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 )
99 98 adantr ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 )
100 r19.26 ⊢ ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) ↔ ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) )
101 78 99 100 sylanbrc ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) )
102 73 101 jca ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) ) )
103 eleq1 ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ) )
104 103 notbid ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ↔ ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ) )
105 eqeq1 ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ) )
106 105 notbid ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ) )
107 106 ralbidv ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ) )
108 eqeq1 ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ↔ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
109 108 notbid ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ↔ ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
110 109 ralbidv ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ↔ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
111 107 110 anbi12d ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) ↔ ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
112 111 ralbidv ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) ↔ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
113 104 112 anbi12d ⊢ ( ∀𝑔 𝑖 𝑢 = 𝑓 → ( ( ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
114 113 eqcoms ⊢ ( 𝑓 = ∀𝑔 𝑖 𝑢 → ( ( ¬ ∀𝑔 𝑖 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ∀𝑔 𝑖 𝑢 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
115 102 114 syl5ibcom ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( 𝑓 = ∀𝑔 𝑖 𝑢 → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
116 115 rexlimdva ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ( ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
117 67 116 jaod ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
118 117 rexlimdva ⊢ ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
119 elndif ⊢ ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → ¬ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
120 119 adantl ⊢ ( ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
121 120 intnand ⊢ ( ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) )
122 11 121 syl ⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) )
123 122 ex ⊢ ( 𝑁 ∈ ω → ( ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) → ¬ ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) ) )
124 123 con2d ⊢ ( 𝑁 ∈ ω → ( ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ) )
125 124 impl ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) )
126 elneeldif ⊢ ( ( 𝑏 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → 𝑏 ≠ 𝑣 )
127 126 necomd ⊢ ( ( 𝑏 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → 𝑣 ≠ 𝑏 )
128 127 ancoms ⊢ ( ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑣 ≠ 𝑏 )
129 128 neneqd ⊢ ( ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ 𝑣 = 𝑏 )
130 129 olcd ⊢ ( ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) → ( ¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏 ) )
131 130 28 sylibr ⊢ ( ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
132 131 intnand ⊢ ( ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 1o = 1o ∧ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
133 132 40 sylnibr ⊢ ( ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
134 133 ralrimiva ⊢ ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
135 134 ralrimivw ⊢ ( 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
136 135 adantl ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) )
137 48 a1i ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 )
138 137 ralrimivw ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 )
139 138 ralrimivw ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 )
140 136 139 52 sylanbrc ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) )
141 125 140 jca ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) )
142 eleq1 ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ) )
143 142 notbid ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ↔ ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ) )
144 eqeq1 ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ↔ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ) )
145 144 notbid ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ) )
146 145 ralbidv ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ) )
147 eqeq1 ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ↔ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
148 147 notbid ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ↔ ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
149 148 ralbidv ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ↔ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
150 146 149 anbi12d ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ↔ ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
151 150 ralbidv ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ↔ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
152 143 151 anbi12d ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = 𝑓 → ( ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
153 152 eqcoms ⊢ ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ( ¬ ( 𝑢 ⊼𝑔 𝑣 ) ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
154 141 153 syl5ibcom ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) → ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
155 154 rexlimdva ⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
156 155 rexlimdva ⊢ ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
157 118 156 jaod ⊢ ( 𝑁 ∈ ω → ( ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) → ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
158 isfmlasuc ⊢ ( ( 𝑁 ∈ ω ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
159 158 elvd ⊢ ( 𝑁 ∈ ω → ( 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
160 159 notbid ⊢ ( 𝑁 ∈ ω → ( ¬ 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ¬ ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
161 ioran ⊢ ( ¬ ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ¬ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
162 ralnex ⊢ ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ↔ ¬ ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) )
163 ralnex ⊢ ( ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ↔ ¬ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 )
164 162 163 anbi12i ⊢ ( ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ( ¬ ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ¬ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) )
165 ioran ⊢ ( ¬ ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ( ¬ ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ¬ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) )
166 164 165 bitr4i ⊢ ( ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ¬ ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) )
167 166 ralbii ⊢ ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ¬ ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) )
168 ralnex ⊢ ( ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ¬ ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ¬ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) )
169 167 168 bitr2i ⊢ ( ¬ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ↔ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) )
170 169 anbi2i ⊢ ( ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ¬ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
171 161 170 bitri ⊢ ( ¬ ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑏 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∨ ∃ 𝑗 ∈ ω 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) )
172 160 171 bitrdi ⊢ ( 𝑁 ∈ ω → ( ¬ 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ( ¬ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∧ ∀ 𝑎 ∈ ( Fmla ‘ 𝑁 ) ( ∀ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ¬ 𝑓 = ( 𝑎 ⊼𝑔 𝑏 ) ∧ ∀ 𝑗 ∈ ω ¬ 𝑓 = ∀𝑔 𝑗 𝑎 ) ) ) )
173 157 172 sylibrd ⊢ ( 𝑁 ∈ ω → ( ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ) → ¬ 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) ) )
174 10 173 biimtrid ⊢ ( 𝑁 ∈ ω → ( 𝑓 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } → ¬ 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) ) )
175 174 ralrimiv ⊢ ( 𝑁 ∈ ω → ∀ 𝑓 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } ¬ 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) )
176 disjr ⊢ ( ( ( Fmla ‘ suc 𝑁 ) ∩ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } ) = ∅ ↔ ∀ 𝑓 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } ¬ 𝑓 ∈ ( Fmla ‘ suc 𝑁 ) )
177 175 176 sylibr ⊢ ( 𝑁 ∈ ω → ( ( Fmla ‘ suc 𝑁 ) ∩ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) } ) = ∅ )