Theorem fmlasucdisj 32646

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 3497	. . . . 5 ⊢ 𝑓 ∈ V
2		eqeq1 2825	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 𝑓 = (𝑢⊼𝑔𝑣)))
3	2	rexbidv 3297	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣)))
4		eqeq1 2825	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = ∀𝑔𝑖𝑢 ↔ 𝑓 = ∀𝑔𝑖𝑢))
5	4	rexbidv 3297	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢))
6	3, 5	orbi12d 915	. . . . . . 7 ⊢ (𝑥 = 𝑓 → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
7	6	rexbidv 3297	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
8	2	2rexbidv 3300	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
9	7, 8	orbi12d 915	. . . . 5 ⊢ (𝑥 = 𝑓 → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣)) ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣))))
10	1, 9	elab 3667	. . . 4 ⊢ (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
11		gonar 32642	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)))
12		elndif 4105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
13	12	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
14	13	intnanrd 492	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
15	11, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
16	15	ex 415	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁))))
17	16	con2d 136	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
18	17	impl 458	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
19		elneeldif 3950	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑎 ≠ 𝑢)
20	19	necomd 3071	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑢 ≠ 𝑎)
21	20	ancoms 461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → 𝑢 ≠ 𝑎)
22	21	neneqd 3021	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ 𝑢 = 𝑎)
23	22	orcd 869	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
24		ianor 978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
25		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
26		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
27	25, 26	opth 5368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏))
28	24, 27	xchnxbir 335	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
29	23, 28	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
30	29	olcd 870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
31		ianor 978	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
32		gonafv 32597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
33	32	el2v 3501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
34		gonafv 32597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
35	34	el2v 3501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩
36	33, 35	eqeq12i 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
37		1oex 8110	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
38		opex 5356	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑢, 𝑣⟩ ∈ V
39	37, 38	opth 5368	. . . . . . . . . . . . . . . . . . 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 3183	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
44	43	ralrimiva 3182	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
45	44	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
46	45	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
47		gonanegoal 32599	. . . . . . . . . . . . . . . 16 ⊢ (𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑗𝑎
48	47	neii 3018	. . . . . . . . . . . . . . 15 ⊢ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
50	49	ralrimivw 3183	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
51	50	ralrimivw 3183	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
52		r19.26 3170	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
53	46, 51, 52	sylanbrc 585	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
54	18, 53	jca 514	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
55		eleq1 2900	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 ∈ (Fmla‘𝑁) ↔ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
56	55	notbid 320	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ↔ ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
57		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = (𝑎⊼𝑔𝑏) ↔ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
58	57	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
59	58	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
60		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = ∀𝑔𝑗𝑎 ↔ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
61	60	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
62	61	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
63	59, 62	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
64	63	ralbidv 3197	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
65	56, 64	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))))
66	54, 65	syl5ibrcom 249	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
67	66	rexlimdva 3284	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
68		goalr 32644	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → 𝑢 ∈ (Fmla‘𝑁))
69	68, 12	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
70	69	ex 415	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ω → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
71	70	con2d 136	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)))
72	71	imp 409	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
73	72	adantr 483	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
74		gonanegoal 32599	. . . . . . . . . . . . . . . 16 ⊢ (𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢
75	74	nesymi 3073	. . . . . . . . . . . . . . 15 ⊢ ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏)
76	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
77	76	ralrimivw 3183	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
78	77	ralrimivw 3183	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
79	22	olcd 870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
80		ianor 978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎) ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
81		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
82	81, 25	opth 5368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎))
83	80, 82	xchnxbir 335	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
84	79, 83	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩)
85	84	olcd 870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
86		ianor 978	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩) ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
87		2oex 8112	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
88		opex 5356	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑖, 𝑢⟩ ∈ V
89	87, 88	opth 5368	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
90	86, 89	xchnxbir 335	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
91		df-goal 32589	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
92		df-goal 32589	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑗𝑎 = ⟨2o, ⟨𝑗, 𝑎⟩⟩
93	91, 92	eqeq12i 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩)
94	90, 93	xchnxbir 335	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
95	85, 94	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
96	95	ralrimivw 3183	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
97	96	ralrimiva 3182	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
98	97	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
99	98	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
100		r19.26 3170	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
101	78, 99, 100	sylanbrc 585	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
102	73, 101	jca 514	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)))
103		eleq1 2900	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
104	103	notbid 320	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
105		eqeq1 2825	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
106	105	notbid 320	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
107	106	ralbidv 3197	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
108		eqeq1 2825	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
109	108	notbid 320	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
110	109	ralbidv 3197	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
111	107, 110	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
112	111	ralbidv 3197	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
113	104, 112	anbi12d 632	. . . . . . . . . . 11 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
114	113	eqcoms 2829	. . . . . . . . . 10 ⊢ (𝑓 = ∀𝑔𝑖𝑢 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
115	102, 114	syl5ibcom 247	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
116	115	rexlimdva 3284	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
117	67, 116	jaod 855	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
118	117	rexlimdva 3284	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
119		elndif 4105	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (Fmla‘𝑁) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
120	119	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
121	120	intnand 491	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
122	11, 121	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
123	122	ex 415	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))))
124	123	con2d 136	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
125	124	impl 458	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
126		elneeldif 3950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑏 ≠ 𝑣)
127	126	necomd 3071	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑣 ≠ 𝑏)
128	127	ancoms 461	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → 𝑣 ≠ 𝑏)
129	128	neneqd 3021	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ 𝑣 = 𝑏)
130	129	olcd 870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
131	130, 28	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
132	131	intnand 491	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
133	132, 40	sylnibr 331	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
134	133	ralrimiva 3182	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
135	134	ralrimivw 3183	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
136	135	adantl 484	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
137	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
138	137	ralrimivw 3183	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
139	138	ralrimivw 3183	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
140	136, 139, 52	sylanbrc 585	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
141	125, 140	jca 514	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
142		eleq1 2900	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
143	142	notbid 320	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
144		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
145	144	notbid 320	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
146	145	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
147		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
148	147	notbid 320	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
149	148	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
150	146, 149	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
151	150	ralbidv 3197	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
152	143, 151	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
153	152	eqcoms 2829	. . . . . . . . 9 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
154	141, 153	syl5ibcom 247	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
155	154	rexlimdva 3284	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
156	155	rexlimdva 3284	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
157	118, 156	jaod 855	. . . . 5 ⊢ (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
158		isfmlasuc 32635	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑓 ∈ V) → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
159	158	elvd 3500	. . . . . . 7 ⊢ (𝑁 ∈ ω → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
160	159	notbid 320	. . . . . 6 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ ¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
161		ioran 980	. . . . . . 7 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)))
162		ralnex 3236	. . . . . . . . . . . 12 ⊢ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏))
163		ralnex 3236	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)
164	162, 163	anbi12i 628	. . . . . . . . . . 11 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
165		ioran 980	. . . . . . . . . . 11 ⊢ (¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
166	164, 165	bitr4i 280	. . . . . . . . . 10 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
167	166	ralbii 3165	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
168		ralnex 3236	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
169	167, 168	bitr2i 278	. . . . . . . 8 ⊢ (¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
170	169	anbi2i 624	. . . . . . 7 ⊢ ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
171	161, 170	bitri 277	. . . . . 6 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
172	160, 171	syl6bb 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	syl5bi 244	. . 3 ⊢ (𝑁 ∈ ω → (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
175	174	ralrimiv 3181	. 2 ⊢ (𝑁 ∈ ω → ∀𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ¬ 𝑓 ∈ (Fmla‘suc 𝑁))
176		disjr 4400	. 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 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114  {cab 2799   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  Vcvv 3494   ∖ cdif 3933   ∩ cin 3935  ∅c0 4291  ⟨cop 4573  suc csuc 6193  ‘cfv 6355  (class class class)co 7156  ωcom 7580  1_oc1o 8095  2_oc2o 8096  ⊼_𝑔cgna 32581  ∀_𝑔cgol 32582  Fmlacfmla 32584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-2o 8103  df-map 8408  df-goel 32587  df-gona 32588  df-goal 32589  df-sat 32590  df-fmla 32592

This theorem is referenced by:  satffunlem2lem2  32653