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 syl5bi ( 𝑁 ∈ ω → ( 𝑓 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( 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 ‘ 𝑁 ) ) 𝑥 = ( 𝑢𝑔 𝑣 ) ) } ) = ∅ )