Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmlasucdisj Structured version   Visualization version   GIF version

Theorem fmlasucdisj 35405
Description: The valid Godel formulas of height (𝑁 + 1) is disjoint with the difference ((Fmla‘suc suc 𝑁) ∖ (Fmla‘suc 𝑁)), 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 (𝑁 + 1). (Contributed by AV, 20-Oct-2023.)
Assertion
Ref Expression
fmlasucdisj (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))}) = ∅)
Distinct variable group:   𝑖,𝑁,𝑢,𝑣,𝑥

Proof of Theorem fmlasucdisj
Dummy variables 𝑎 𝑏 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3483 . . . . 5 𝑓 ∈ V
2 eqeq1 2740 . . . . . . . . 9 (𝑥 = 𝑓 → (𝑥 = (𝑢𝑔𝑣) ↔ 𝑓 = (𝑢𝑔𝑣)))
32rexbidv 3178 . . . . . . . 8 (𝑥 = 𝑓 → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣)))
4 eqeq1 2740 . . . . . . . . 9 (𝑥 = 𝑓 → (𝑥 = ∀𝑔𝑖𝑢𝑓 = ∀𝑔𝑖𝑢))
54rexbidv 3178 . . . . . . . 8 (𝑥 = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢))
63, 5orbi12d 918 . . . . . . 7 (𝑥 = 𝑓 → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
76rexbidv 3178 . . . . . 6 (𝑥 = 𝑓 → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
822rexbidv 3221 . . . . . 6 (𝑥 = 𝑓 → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣) ↔ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣)))
97, 8orbi12d 918 . . . . 5 (𝑥 = 𝑓 → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣)) ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣))))
101, 9elab 3678 . . . 4 (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))} ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣)))
11 gonar 35401 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ω ∧ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)) → (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)))
12 elndif 4132 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
1312adantr 480 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
1413intnanrd 489 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
1511, 14syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ω ∧ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
1615ex 412 . . . . . . . . . . . . 13 (𝑁 ∈ ω → ((𝑢𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁))))
1716con2d 134 . . . . . . . . . . . 12 (𝑁 ∈ ω → ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)))
1817impl 455 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁))
19 elneeldif 3964 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑎𝑢)
2019necomd 2995 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑢𝑎)
2120ancoms 458 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → 𝑢𝑎)
2221neneqd 2944 . . . . . . . . . . . . . . . . . . . 20 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ 𝑢 = 𝑎)
2322orcd 873 . . . . . . . . . . . . . . . . . . 19 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
24 ianor 983 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝑢 = 𝑎𝑣 = 𝑏) ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
25 vex 3483 . . . . . . . . . . . . . . . . . . . . 21 𝑢 ∈ V
26 vex 3483 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
2725, 26opth 5480 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑢 = 𝑎𝑣 = 𝑏))
2824, 27xchnxbir 333 . . . . . . . . . . . . . . . . . . 19 (¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
2923, 28sylibr 234 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
3029olcd 874 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
31 ianor 983 . . . . . . . . . . . . . . . . . 18 (¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
32 gonafv 35356 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
3332el2v 3486 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
34 gonafv 35356 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
3534el2v 3486 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩
3633, 35eqeq12i 2754 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑔𝑣) = (𝑎𝑔𝑏) ↔ ⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
37 1oex 8517 . . . . . . . . . . . . . . . . . . . 20 1o ∈ V
38 opex 5468 . . . . . . . . . . . . . . . . . . . 20 𝑢, 𝑣⟩ ∈ V
3937, 38opth 5480 . . . . . . . . . . . . . . . . . . 19 (⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩ ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
4036, 39bitri 275 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑔𝑣) = (𝑎𝑔𝑏) ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
4131, 40xchnxbir 333 . . . . . . . . . . . . . . . . 17 (¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
4230, 41sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
4342ralrimivw 3149 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
4443ralrimiva 3145 . . . . . . . . . . . . . 14 (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
4544adantl 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
4645adantr 480 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
47 gonanegoal 35358 . . . . . . . . . . . . . . . 16 (𝑢𝑔𝑣) ≠ ∀𝑔𝑗𝑎
4847neii 2941 . . . . . . . . . . . . . . 15 ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎
4948a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)
5049ralrimivw 3149 . . . . . . . . . . . . 13 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)
5150ralrimivw 3149 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)
52 r19.26 3110 . . . . . . . . . . . 12 (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))
5346, 51, 52sylanbrc 583 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))
5418, 53jca 511 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)))
55 eleq1 2828 . . . . . . . . . . . 12 (𝑓 = (𝑢𝑔𝑣) → (𝑓 ∈ (Fmla‘𝑁) ↔ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)))
5655notbid 318 . . . . . . . . . . 11 (𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ↔ ¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)))
57 eqeq1 2740 . . . . . . . . . . . . . . 15 (𝑓 = (𝑢𝑔𝑣) → (𝑓 = (𝑎𝑔𝑏) ↔ (𝑢𝑔𝑣) = (𝑎𝑔𝑏)))
5857notbid 318 . . . . . . . . . . . . . 14 (𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 = (𝑎𝑔𝑏) ↔ ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏)))
5958ralbidv 3177 . . . . . . . . . . . . 13 (𝑓 = (𝑢𝑔𝑣) → (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏)))
60 eqeq1 2740 . . . . . . . . . . . . . . 15 (𝑓 = (𝑢𝑔𝑣) → (𝑓 = ∀𝑔𝑗𝑎 ↔ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))
6160notbid 318 . . . . . . . . . . . . . 14 (𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))
6261ralbidv 3177 . . . . . . . . . . . . 13 (𝑓 = (𝑢𝑔𝑣) → (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))
6359, 62anbi12d 632 . . . . . . . . . . . 12 (𝑓 = (𝑢𝑔𝑣) → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)))
6463ralbidv 3177 . . . . . . . . . . 11 (𝑓 = (𝑢𝑔𝑣) → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)))
6556, 64anbi12d 632 . . . . . . . . . 10 (𝑓 = (𝑢𝑔𝑣) → ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))))
6654, 65syl5ibrcom 247 . . . . . . . . 9 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
6766rexlimdva 3154 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
68 goalr 35403 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → 𝑢 ∈ (Fmla‘𝑁))
6968, 12syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
7069ex 412 . . . . . . . . . . . . . 14 (𝑁 ∈ ω → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
7170con2d 134 . . . . . . . . . . . . 13 (𝑁 ∈ ω → (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)))
7271imp 406 . . . . . . . . . . . 12 ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
7372adantr 480 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
74 gonanegoal 35358 . . . . . . . . . . . . . . . 16 (𝑎𝑔𝑏) ≠ ∀𝑔𝑖𝑢
7574nesymi 2997 . . . . . . . . . . . . . . 15 ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏)
7675a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏))
7776ralrimivw 3149 . . . . . . . . . . . . 13 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏))
7877ralrimivw 3149 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏))
7922olcd 874 . . . . . . . . . . . . . . . . . . 19 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
80 ianor 983 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝑖 = 𝑗𝑢 = 𝑎) ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
81 vex 3483 . . . . . . . . . . . . . . . . . . . . 21 𝑖 ∈ V
8281, 25opth 5480 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (𝑖 = 𝑗𝑢 = 𝑎))
8380, 82xchnxbir 333 . . . . . . . . . . . . . . . . . . 19 (¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
8479, 83sylibr 234 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩)
8584olcd 874 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
86 ianor 983 . . . . . . . . . . . . . . . . . . 19 (¬ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩) ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
87 2oex 8518 . . . . . . . . . . . . . . . . . . . 20 2o ∈ V
88 opex 5468 . . . . . . . . . . . . . . . . . . . 20 𝑖, 𝑢⟩ ∈ V
8987, 88opth 5480 . . . . . . . . . . . . . . . . . . 19 (⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
9086, 89xchnxbir 333 . . . . . . . . . . . . . . . . . 18 (¬ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
91 df-goal 35348 . . . . . . . . . . . . . . . . . . 19 𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
92 df-goal 35348 . . . . . . . . . . . . . . . . . . 19 𝑔𝑗𝑎 = ⟨2o, ⟨𝑗, 𝑎⟩⟩
9391, 92eqeq12i 2754 . . . . . . . . . . . . . . . . . 18 (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩)
9490, 93xchnxbir 333 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
9585, 94sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
9695ralrimivw 3149 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
9796ralrimiva 3145 . . . . . . . . . . . . . 14 (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
9897adantl 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
9998adantr 480 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
100 r19.26 3110 . . . . . . . . . . . 12 (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
10178, 99, 100sylanbrc 583 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
10273, 101jca 511 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)))
103 eleq1 2828 . . . . . . . . . . . . 13 (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
104103notbid 318 . . . . . . . . . . . 12 (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
105 eqeq1 2740 . . . . . . . . . . . . . . . 16 (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ↔ 𝑓 = (𝑎𝑔𝑏)))
106105notbid 318 . . . . . . . . . . . . . . 15 (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ↔ ¬ 𝑓 = (𝑎𝑔𝑏)))
107106ralbidv 3177 . . . . . . . . . . . . . 14 (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏)))
108 eqeq1 2740 . . . . . . . . . . . . . . . 16 (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎𝑓 = ∀𝑔𝑗𝑎))
109108notbid 318 . . . . . . . . . . . . . . 15 (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
110109ralbidv 3177 . . . . . . . . . . . . . 14 (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
111107, 110anbi12d 632 . . . . . . . . . . . . 13 (∀𝑔𝑖𝑢 = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
112111ralbidv 3177 . . . . . . . . . . . 12 (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
113104, 112anbi12d 632 . . . . . . . . . . 11 (∀𝑔𝑖𝑢 = 𝑓 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
114113eqcoms 2744 . . . . . . . . . 10 (𝑓 = ∀𝑔𝑖𝑢 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
115102, 114syl5ibcom 245 . . . . . . . . 9 (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
116115rexlimdva 3154 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
11767, 116jaod 859 . . . . . . 7 ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
118117rexlimdva 3154 . . . . . 6 (𝑁 ∈ ω → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
119 elndif 4132 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (Fmla‘𝑁) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
120119adantl 481 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
121120intnand 488 . . . . . . . . . . . . . 14 ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
12211, 121syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ω ∧ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
123122ex 412 . . . . . . . . . . . 12 (𝑁 ∈ ω → ((𝑢𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))))
124123con2d 134 . . . . . . . . . . 11 (𝑁 ∈ ω → ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁)))
125124impl 455 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁))
126 elneeldif 3964 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑏𝑣)
127126necomd 2995 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑣𝑏)
128127ancoms 458 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → 𝑣𝑏)
129128neneqd 2944 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ 𝑣 = 𝑏)
130129olcd 874 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
131130, 28sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
132131intnand 488 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
133132, 40sylnibr 329 . . . . . . . . . . . . . 14 ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
134133ralrimiva 3145 . . . . . . . . . . . . 13 (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
135134ralrimivw 3149 . . . . . . . . . . . 12 (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
136135adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏))
13748a1i 11 . . . . . . . . . . . . 13 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)
138137ralrimivw 3149 . . . . . . . . . . . 12 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)
139138ralrimivw 3149 . . . . . . . . . . 11 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)
140136, 139, 52sylanbrc 583 . . . . . . . . . 10 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎))
141125, 140jca 511 . . . . . . . . 9 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)))
142 eleq1 2828 . . . . . . . . . . . 12 ((𝑢𝑔𝑣) = 𝑓 → ((𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
143142notbid 318 . . . . . . . . . . 11 ((𝑢𝑔𝑣) = 𝑓 → (¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
144 eqeq1 2740 . . . . . . . . . . . . . . 15 ((𝑢𝑔𝑣) = 𝑓 → ((𝑢𝑔𝑣) = (𝑎𝑔𝑏) ↔ 𝑓 = (𝑎𝑔𝑏)))
145144notbid 318 . . . . . . . . . . . . . 14 ((𝑢𝑔𝑣) = 𝑓 → (¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ↔ ¬ 𝑓 = (𝑎𝑔𝑏)))
146145ralbidv 3177 . . . . . . . . . . . . 13 ((𝑢𝑔𝑣) = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏)))
147 eqeq1 2740 . . . . . . . . . . . . . . 15 ((𝑢𝑔𝑣) = 𝑓 → ((𝑢𝑔𝑣) = ∀𝑔𝑗𝑎𝑓 = ∀𝑔𝑗𝑎))
148147notbid 318 . . . . . . . . . . . . . 14 ((𝑢𝑔𝑣) = 𝑓 → (¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
149148ralbidv 3177 . . . . . . . . . . . . 13 ((𝑢𝑔𝑣) = 𝑓 → (∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
150146, 149anbi12d 632 . . . . . . . . . . . 12 ((𝑢𝑔𝑣) = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
151150ralbidv 3177 . . . . . . . . . . 11 ((𝑢𝑔𝑣) = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
152143, 151anbi12d 632 . . . . . . . . . 10 ((𝑢𝑔𝑣) = 𝑓 → ((¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
153152eqcoms 2744 . . . . . . . . 9 (𝑓 = (𝑢𝑔𝑣) → ((¬ (𝑢𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢𝑔𝑣) = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
154141, 153syl5ibcom 245 . . . . . . . 8 (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
155154rexlimdva 3154 . . . . . . 7 ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
156155rexlimdva 3154 . . . . . 6 (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
157118, 156jaod 859 . . . . 5 (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣)) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
158 isfmlasuc 35394 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑓 ∈ V) → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
159158elvd 3485 . . . . . . 7 (𝑁 ∈ ω → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
160159notbid 318 . . . . . 6 (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ ¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
161 ioran 985 . . . . . . 7 (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)))
162 ralnex 3071 . . . . . . . . . . . 12 (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ↔ ¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏))
163 ralnex 3071 . . . . . . . . . . . 12 (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)
164162, 163anbi12i 628 . . . . . . . . . . 11 ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
165 ioran 985 . . . . . . . . . . 11 (¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
166164, 165bitr4i 278 . . . . . . . . . 10 ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
167166ralbii 3092 . . . . . . . . 9 (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
168 ralnex 3071 . . . . . . . . 9 (∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
169167, 168bitr2i 276 . . . . . . . 8 (¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
170169anbi2i 623 . . . . . . 7 ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
171161, 170bitri 275 . . . . . 6 (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
172160, 171bitrdi 287 . . . . 5 (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
173157, 172sylibrd 259 . . . 4 (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢𝑔𝑣)) → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
17410, 173biimtrid 242 . . 3 (𝑁 ∈ ω → (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))} → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
175174ralrimiv 3144 . 2 (𝑁 ∈ ω → ∀𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))} ¬ 𝑓 ∈ (Fmla‘suc 𝑁))
176 disjr 4450 . 2 (((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))}) = ∅ ↔ ∀𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))} ¬ 𝑓 ∈ (Fmla‘suc 𝑁))
177175, 176sylibr 234 1 (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢𝑔𝑣))}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1539  wcel 2107  {cab 2713  wne 2939  wral 3060  wrex 3069  Vcvv 3479  cdif 3947  cin 3949  c0 4332  cop 4631  suc csuc 6385  cfv 6560  (class class class)co 7432  ωcom 7888  1oc1o 8500  2oc2o 8501  𝑔cgna 35340  𝑔cgol 35341  Fmlacfmla 35343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-map 8869  df-goel 35346  df-gona 35347  df-goal 35348  df-sat 35349  df-fmla 35351
This theorem is referenced by:  satffunlem2lem2  35412
  Copyright terms: Public domain W3C validator