Theorem fmlasucdisj 35709

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 3457	. . . . 5 ⊢ 𝑓 ∈ V
2		eqeq1 2765	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 𝑓 = (𝑢⊼𝑔𝑣)))
3	2	rexbidv 3185	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣)))
4		eqeq1 2765	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = ∀𝑔𝑖𝑢 ↔ 𝑓 = ∀𝑔𝑖𝑢))
5	4	rexbidv 3185	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢))
6	3, 5	orbi12d 929	. . . . . . 7 ⊢ (𝑥 = 𝑓 → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
7	6	rexbidv 3185	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
8	2	2rexbidv 3226	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
9	7, 8	orbi12d 929	. . . . 5 ⊢ (𝑥 = 𝑓 → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣)) ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣))))
10	1, 9	elab 3637	. . . 4 ⊢ (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
11		gonar 35705	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)))
12		elndif 4084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
13	12	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
14	13	intnanrd 493	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
15	11, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
16	15	ex 416	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁))))
17	16	con2d 134	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
18	17	impl 459	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
19		elneeldif 3916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑎 ≠ 𝑢)
20	19	necomd 3011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑢 ≠ 𝑎)
21	20	ancoms 462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → 𝑢 ≠ 𝑎)
22	21	neneqd 2961	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ 𝑢 = 𝑎)
23	22	orcd 884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
24		ianor 994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
25		vex 3457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
26		vex 3457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
27	25, 26	opth 5441	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏))
28	24, 27	xchnxbir 335	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
29	23, 28	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
30	29	olcd 885	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
31		ianor 994	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
32		gonafv 35660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
33	32	el2v 3460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
34		gonafv 35660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
35	34	el2v 3460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩
36	33, 35	eqeq12i 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
37		1oex 8440	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
38		opex 5428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑢, 𝑣⟩ ∈ V
39	37, 38	opth 5441	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩ ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
40	36, 39	bitri 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
41	31, 40	xchnxbir 335	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
42	30, 41	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
43	42	ralrimivw 3157	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
44	43	ralrimiva 3153	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
45	44	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
46	45	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
47		gonanegoal 35662	. . . . . . . . . . . . . . . 16 ⊢ (𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑗𝑎
48	47	neii 2958	. . . . . . . . . . . . . . 15 ⊢ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
50	49	ralrimivw 3157	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
51	50	ralrimivw 3157	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
52		r19.26 3121	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
53	46, 51, 52	sylanbrc 592	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
54	18, 53	jca 519	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
55		eleq1 2849	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 ∈ (Fmla‘𝑁) ↔ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
56	55	notbid 320	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ↔ ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
57		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = (𝑎⊼𝑔𝑏) ↔ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
58	57	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
59	58	ralbidv 3184	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
60		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = ∀𝑔𝑗𝑎 ↔ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
61	60	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
62	61	ralbidv 3184	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
63	59, 62	anbi12d 641	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
64	63	ralbidv 3184	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
65	56, 64	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))))
66	54, 65	syl5ibrcom 249	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
67	66	rexlimdva 3162	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
68		goalr 35707	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → 𝑢 ∈ (Fmla‘𝑁))
69	68, 12	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
70	69	ex 416	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ω → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
71	70	con2d 134	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)))
72	71	imp 410	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
73	72	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
74		gonanegoal 35662	. . . . . . . . . . . . . . . 16 ⊢ (𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢
75	74	nesymi 3013	. . . . . . . . . . . . . . 15 ⊢ ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏)
76	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
77	76	ralrimivw 3157	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
78	77	ralrimivw 3157	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
79	22	olcd 885	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
80		ianor 994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎) ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
81		vex 3457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
82	81, 25	opth 5441	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎))
83	80, 82	xchnxbir 335	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
84	79, 83	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩)
85	84	olcd 885	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
86		ianor 994	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩) ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
87		2oex 8442	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
88		opex 5428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑖, 𝑢⟩ ∈ V
89	87, 88	opth 5441	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
90	86, 89	xchnxbir 335	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
91		df-goal 35652	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
92		df-goal 35652	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑗𝑎 = ⟨2o, ⟨𝑗, 𝑎⟩⟩
93	91, 92	eqeq12i 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩)
94	90, 93	xchnxbir 335	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
95	85, 94	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
96	95	ralrimivw 3157	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
97	96	ralrimiva 3153	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
98	97	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
99	98	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
100		r19.26 3121	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
101	78, 99, 100	sylanbrc 592	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
102	73, 101	jca 519	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)))
103		eleq1 2849	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
104	103	notbid 320	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
105		eqeq1 2765	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
106	105	notbid 320	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
107	106	ralbidv 3184	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
108		eqeq1 2765	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
109	108	notbid 320	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
110	109	ralbidv 3184	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
111	107, 110	anbi12d 641	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
112	111	ralbidv 3184	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
113	104, 112	anbi12d 641	. . . . . . . . . . 11 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
114	113	eqcoms 2769	. . . . . . . . . 10 ⊢ (𝑓 = ∀𝑔𝑖𝑢 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
115	102, 114	syl5ibcom 247	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
116	115	rexlimdva 3162	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
117	67, 116	jaod 870	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
118	117	rexlimdva 3162	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
119		elndif 4084	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (Fmla‘𝑁) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
120	119	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
121	120	intnand 492	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
122	11, 121	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
123	122	ex 416	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))))
124	123	con2d 134	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
125	124	impl 459	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
126		elneeldif 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑏 ≠ 𝑣)
127	126	necomd 3011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑣 ≠ 𝑏)
128	127	ancoms 462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → 𝑣 ≠ 𝑏)
129	128	neneqd 2961	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ 𝑣 = 𝑏)
130	129	olcd 885	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
131	130, 28	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
132	131	intnand 492	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
133	132, 40	sylnibr 331	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
134	133	ralrimiva 3153	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
135	134	ralrimivw 3157	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
136	135	adantl 485	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
137	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
138	137	ralrimivw 3157	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
139	138	ralrimivw 3157	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
140	136, 139, 52	sylanbrc 592	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
141	125, 140	jca 519	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
142		eleq1 2849	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
143	142	notbid 320	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
144		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
145	144	notbid 320	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
146	145	ralbidv 3184	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
147		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
148	147	notbid 320	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
149	148	ralbidv 3184	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
150	146, 149	anbi12d 641	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
151	150	ralbidv 3184	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
152	143, 151	anbi12d 641	. . . . . . . . . 10 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
153	152	eqcoms 2769	. . . . . . . . 9 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
154	141, 153	syl5ibcom 247	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
155	154	rexlimdva 3162	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
156	155	rexlimdva 3162	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
157	118, 156	jaod 870	. . . . 5 ⊢ (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
158		isfmlasuc 35698	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑓 ∈ V) → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
159	158	elvd 3459	. . . . . . 7 ⊢ (𝑁 ∈ ω → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
160	159	notbid 320	. . . . . 6 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ ¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
161		ioran 996	. . . . . . 7 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)))
162		ralnex 3087	. . . . . . . . . . . 12 ⊢ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏))
163		ralnex 3087	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)
164	162, 163	anbi12i 637	. . . . . . . . . . 11 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
165		ioran 996	. . . . . . . . . . 11 ⊢ (¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
166	164, 165	bitr4i 280	. . . . . . . . . 10 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
167	166	ralbii 3107	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
168		ralnex 3087	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
169	167, 168	bitr2i 278	. . . . . . . 8 ⊢ (¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
170	169	anbi2i 632	. . . . . . 7 ⊢ ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
171	161, 170	bitri 277	. . . . . 6 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
172	160, 171	bitrdi 289	. . . . 5 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
173	157, 172	sylibrd 261	. . . 4 ⊢ (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)) → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
174	10, 173	biimtrid 244	. . 3 ⊢ (𝑁 ∈ ω → (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
175	174	ralrimiv 3152	. 2 ⊢ (𝑁 ∈ ω → ∀𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ¬ 𝑓 ∈ (Fmla‘suc 𝑁))
176		disjr 4402	. 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 236	1 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1559   ∈ wcel 2141  {cab 2739   ≠ wne 2956  ∀wral 3075  ∃wrex 3085  Vcvv 3453   ∖ cdif 3899   ∩ cin 3901  ∅c0 4283  ⟨cop 4585  suc csuc 6342  ‘cfv 6515  (class class class)co 7390  ωcom 7840  1_oc1o 8423  2_oc2o 8424  ⊼_𝑔cgna 35644  ∀_𝑔cgol 35645  Fmlacfmla 35647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-inf2 9589

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7841  df-1st 7964  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-1o 8430  df-2o 8431  df-map 8803  df-goel 35650  df-gona 35651  df-goal 35652  df-sat 35653  df-fmla 35655

This theorem is referenced by:  satffunlem2lem2  35716