Theorem fmlasucdisj 35757

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.

Step	Hyp	Ref	Expression
1		vex 3461	. . . . 5 ⊢ 𝑓 ∈ V
2		eqeq1 2769	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 𝑓 = (𝑢⊼𝑔𝑣)))
3	2	rexbidv 3189	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣)))
4		eqeq1 2769	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = ∀𝑔𝑖𝑢 ↔ 𝑓 = ∀𝑔𝑖𝑢))
5	4	rexbidv 3189	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢))
6	3, 5	orbi12d 931	. . . . . . 7 ⊢ (𝑥 = 𝑓 → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
7	6	rexbidv 3189	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
8	2	2rexbidv 3230	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
9	7, 8	orbi12d 931	. . . . 5 ⊢ (𝑥 = 𝑓 → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣)) ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣))))
10	1, 9	elab 3641	. . . 4 ⊢ (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
11		gonar 35753	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)))
12		elndif 4089	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
13	12	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
14	13	intnanrd 494	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
15	11, 14	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
16	15	ex 417	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁))))
17	16	con2d 135	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
18	17	impl 460	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
19		elneeldif 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑎 ≠ 𝑢)
20	19	necomd 3015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑢 ≠ 𝑎)
21	20	ancoms 463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → 𝑢 ≠ 𝑎)
22	21	neneqd 2965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ 𝑢 = 𝑎)
23	22	orcd 886	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
24		ianor 997	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
25		vex 3461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
26		vex 3461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
27	25, 26	opth 5448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏))
28	24, 27	xchnxbir 336	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
29	23, 28	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
30	29	olcd 887	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
31		ianor 997	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
32		gonafv 35708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
33	32	el2v 3464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
34		gonafv 35708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
35	34	el2v 3464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩
36	33, 35	eqeq12i 2783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
37		1oex 8451	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
38		opex 5435	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑢, 𝑣⟩ ∈ V
39	37, 38	opth 5448	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩ ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
40	36, 39	bitri 278	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
41	31, 40	xchnxbir 336	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
42	30, 41	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
43	42	ralrimivw 3161	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
44	43	ralrimiva 3157	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
45	44	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
46	45	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
47		gonanegoal 35710	. . . . . . . . . . . . . . . 16 ⊢ (𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑗𝑎
48	47	neii 2962	. . . . . . . . . . . . . . 15 ⊢ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
50	49	ralrimivw 3161	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
51	50	ralrimivw 3161	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
52		r19.26 3125	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
53	46, 51, 52	sylanbrc 594	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
54	18, 53	jca 520	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
55		eleq1 2853	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 ∈ (Fmla‘𝑁) ↔ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
56	55	notbid 321	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ↔ ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
57		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = (𝑎⊼𝑔𝑏) ↔ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
58	57	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
59	58	ralbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
60		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = ∀𝑔𝑗𝑎 ↔ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
61	60	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
62	61	ralbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
63	59, 62	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
64	63	ralbidv 3188	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
65	56, 64	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))))
66	54, 65	syl5ibrcom 250	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
67	66	rexlimdva 3166	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
68		goalr 35755	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → 𝑢 ∈ (Fmla‘𝑁))
69	68, 12	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
70	69	ex 417	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ω → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
71	70	con2d 135	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)))
72	71	imp 411	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
73	72	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
74		gonanegoal 35710	. . . . . . . . . . . . . . . 16 ⊢ (𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢
75	74	nesymi 3017	. . . . . . . . . . . . . . 15 ⊢ ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏)
76	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
77	76	ralrimivw 3161	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
78	77	ralrimivw 3161	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
79	22	olcd 887	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
80		ianor 997	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎) ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
81		vex 3461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
82	81, 25	opth 5448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎))
83	80, 82	xchnxbir 336	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
84	79, 83	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩)
85	84	olcd 887	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
86		ianor 997	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩) ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
87		2oex 8453	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
88		opex 5435	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑖, 𝑢⟩ ∈ V
89	87, 88	opth 5448	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
90	86, 89	xchnxbir 336	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
91		df-goal 35700	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
92		df-goal 35700	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑗𝑎 = ⟨2o, ⟨𝑗, 𝑎⟩⟩
93	91, 92	eqeq12i 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩)
94	90, 93	xchnxbir 336	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
95	85, 94	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
96	95	ralrimivw 3161	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
97	96	ralrimiva 3157	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
98	97	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
99	98	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
100		r19.26 3125	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
101	78, 99, 100	sylanbrc 594	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
102	73, 101	jca 520	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)))
103		eleq1 2853	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
104	103	notbid 321	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
105		eqeq1 2769	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
106	105	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
107	106	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
108		eqeq1 2769	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
109	108	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
110	109	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
111	107, 110	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
112	111	ralbidv 3188	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
113	104, 112	anbi12d 643	. . . . . . . . . . 11 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
114	113	eqcoms 2773	. . . . . . . . . 10 ⊢ (𝑓 = ∀𝑔𝑖𝑢 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
115	102, 114	syl5ibcom 248	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
116	115	rexlimdva 3166	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
117	67, 116	jaod 872	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
118	117	rexlimdva 3166	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
119		elndif 4089	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (Fmla‘𝑁) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
120	119	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
121	120	intnand 493	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
122	11, 121	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
123	122	ex 417	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))))
124	123	con2d 135	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
125	124	impl 460	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
126		elneeldif 3921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑏 ≠ 𝑣)
127	126	necomd 3015	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑣 ≠ 𝑏)
128	127	ancoms 463	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → 𝑣 ≠ 𝑏)
129	128	neneqd 2965	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ 𝑣 = 𝑏)
130	129	olcd 887	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
131	130, 28	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
132	131	intnand 493	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
133	132, 40	sylnibr 332	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
134	133	ralrimiva 3157	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
135	134	ralrimivw 3161	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
136	135	adantl 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
137	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
138	137	ralrimivw 3161	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
139	138	ralrimivw 3161	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
140	136, 139, 52	sylanbrc 594	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
141	125, 140	jca 520	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
142		eleq1 2853	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
143	142	notbid 321	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
144		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
145	144	notbid 321	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
146	145	ralbidv 3188	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
147		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
148	147	notbid 321	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
149	148	ralbidv 3188	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
150	146, 149	anbi12d 643	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
151	150	ralbidv 3188	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
152	143, 151	anbi12d 643	. . . . . . . . . 10 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
153	152	eqcoms 2773	. . . . . . . . 9 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
154	141, 153	syl5ibcom 248	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
155	154	rexlimdva 3166	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
156	155	rexlimdva 3166	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
157	118, 156	jaod 872	. . . . 5 ⊢ (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
158		isfmlasuc 35746	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑓 ∈ V) → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
159	158	elvd 3463	. . . . . . 7 ⊢ (𝑁 ∈ ω → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
160	159	notbid 321	. . . . . 6 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ ¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
161		ioran 999	. . . . . . 7 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)))
162		ralnex 3091	. . . . . . . . . . . 12 ⊢ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏))
163		ralnex 3091	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)
164	162, 163	anbi12i 639	. . . . . . . . . . 11 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
165		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
166	164, 165	bitr4i 281	. . . . . . . . . 10 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
167	166	ralbii 3111	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
168		ralnex 3091	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
169	167, 168	bitr2i 279	. . . . . . . 8 ⊢ (¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
170	169	anbi2i 634	. . . . . . 7 ⊢ ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
171	161, 170	bitri 278	. . . . . 6 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
172	160, 171	bitrdi 290	. . . . 5 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
173	157, 172	sylibrd 262	. . . 4 ⊢ (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)) → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
174	10, 173	biimtrid 245	. . 3 ⊢ (𝑁 ∈ ω → (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
175	174	ralrimiv 3156	. 2 ⊢ (𝑁 ∈ ω → ∀𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ¬ 𝑓 ∈ (Fmla‘suc 𝑁))
176		disjr 4408	. 2 ⊢ (((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 237	1 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1563   ∈ wcel 2145  {cab 2743   ≠ wne 2960  ∀wral 3079  ∃wrex 3089  Vcvv 3457   ∖ cdif 3904   ∩ cin 3906  ∅c0 4288  ⟨cop 4591  suc csuc 6351  ‘cfv 6525  (class class class)co 7400  ωcom 7850  1_oc1o 8434  2_oc2o 8435  ⊼_𝑔cgna 35692  ∀_𝑔cgol 35693  Fmlacfmla 35695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5231  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-inf2 9598

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-map 8814  df-goel 35698  df-gona 35699  df-goal 35700  df-sat 35701  df-fmla 35703

This theorem is referenced by:  satffunlem2lem2  35764