Theorem fmlasucdisj 33261

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 3426	. . . . 5 ⊢ 𝑓 ∈ V
2		eqeq1 2742	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 𝑓 = (𝑢⊼𝑔𝑣)))
3	2	rexbidv 3225	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣)))
4		eqeq1 2742	. . . . . . . . 9 ⊢ (𝑥 = 𝑓 → (𝑥 = ∀𝑔𝑖𝑢 ↔ 𝑓 = ∀𝑔𝑖𝑢))
5	4	rexbidv 3225	. . . . . . . 8 ⊢ (𝑥 = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢))
6	3, 5	orbi12d 915	. . . . . . 7 ⊢ (𝑥 = 𝑓 → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
7	6	rexbidv 3225	. . . . . 6 ⊢ (𝑥 = 𝑓 → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢)))
8	2	2rexbidv 3228	. . . . . 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 3602	. . . 4 ⊢ (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ↔ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)))
11		gonar 33257	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)))
12		elndif 4059	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
13	12	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
14	13	intnanrd 489	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
15	11, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)))
16	15	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁))))
17	16	con2d 134	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
18	17	impl 455	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
19		elneeldif 3897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑎 ≠ 𝑢)
20	19	necomd 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑢 ≠ 𝑎)
21	20	ancoms 458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → 𝑢 ≠ 𝑎)
22	21	neneqd 2947	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ 𝑢 = 𝑎)
23	22	orcd 869	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
24		ianor 978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
25		vex 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
26		vex 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
27	25, 26	opth 5385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑢 = 𝑎 ∧ 𝑣 = 𝑏))
28	24, 27	xchnxbir 332	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩ ↔ (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
29	23, 28	sylibr 233	. . . . . . . . . . . . . . . . . 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 33212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
33	32	el2v 3430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢⊼𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
34		gonafv 33212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
35	34	el2v 3430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎⊼𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩
36	33, 35	eqeq12i 2756	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
37		1oex 8280	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
38		opex 5373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑢, 𝑣⟩ ∈ V
39	37, 38	opth 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1o, ⟨𝑢, 𝑣⟩⟩ = ⟨1o, ⟨𝑎, 𝑏⟩⟩ ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
40	36, 39	bitri 274	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
41	31, 40	xchnxbir 332	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ (¬ 1o = 1o ∨ ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
42	30, 41	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
43	42	ralrimivw 3108	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
44	43	ralrimiva 3107	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
45	44	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
46	45	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
47		gonanegoal 33214	. . . . . . . . . . . . . . . 16 ⊢ (𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑗𝑎
48	47	neii 2944	. . . . . . . . . . . . . . 15 ⊢ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
50	49	ralrimivw 3108	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
51	50	ralrimivw 3108	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
52		r19.26 3094	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
53	46, 51, 52	sylanbrc 582	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
54	18, 53	jca 511	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
55		eleq1 2826	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 ∈ (Fmla‘𝑁) ↔ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
56	55	notbid 317	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ↔ ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
57		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = (𝑎⊼𝑔𝑏) ↔ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
58	57	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
59	58	ralbidv 3120	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏)))
60		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (𝑓 = ∀𝑔𝑗𝑎 ↔ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
61	60	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
62	61	ralbidv 3120	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
63	59, 62	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
64	63	ralbidv 3120	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
65	56, 64	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))))
66	54, 65	syl5ibrcom 246	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
67	66	rexlimdva 3212	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
68		goalr 33259	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → 𝑢 ∈ (Fmla‘𝑁))
69	68, 12	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
70	69	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ω → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) → ¬ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
71	70	con2d 134	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁)))
72	71	imp 406	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
73	72	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁))
74		gonanegoal 33214	. . . . . . . . . . . . . . . 16 ⊢ (𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢
75	74	nesymi 3000	. . . . . . . . . . . . . . 15 ⊢ ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏)
76	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
77	76	ralrimivw 3108	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
78	77	ralrimivw 3108	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏))
79	22	olcd 870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
80		ianor 978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎) ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
81		vex 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
82	81, 25	opth 5385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (𝑖 = 𝑗 ∧ 𝑢 = 𝑎))
83	80, 82	xchnxbir 332	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩ ↔ (¬ 𝑖 = 𝑗 ∨ ¬ 𝑢 = 𝑎))
84	79, 83	sylibr 233	. . . . . . . . . . . . . . . . . 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 8284	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
88		opex 5373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑖, 𝑢⟩ ∈ V
89	87, 88	opth 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
90	86, 89	xchnxbir 332	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩ ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
91		df-goal 33204	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
92		df-goal 33204	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑔𝑗𝑎 = ⟨2o, ⟨𝑗, 𝑎⟩⟩
93	91, 92	eqeq12i 2756	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ⟨2o, ⟨𝑖, 𝑢⟩⟩ = ⟨2o, ⟨𝑗, 𝑎⟩⟩)
94	90, 93	xchnxbir 332	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ (¬ 2o = 2o ∨ ¬ ⟨𝑖, 𝑢⟩ = ⟨𝑗, 𝑎⟩))
95	85, 94	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
96	95	ralrimivw 3108	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑎 ∈ (Fmla‘𝑁)) → ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
97	96	ralrimiva 3107	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
98	97	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
99	98	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)
100		r19.26 3094	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
101	78, 99, 100	sylanbrc 582	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎))
102	73, 101	jca 511	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)))
103		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
104	103	notbid 317	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
105		eqeq1 2742	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
106	105	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
107	106	ralbidv 3120	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
108		eqeq1 2742	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
109	108	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
110	109	ralbidv 3120	. . . . . . . . . . . . . 14 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
111	107, 110	anbi12d 630	. . . . . . . . . . . . 13 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
112	111	ralbidv 3120	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
113	104, 112	anbi12d 630	. . . . . . . . . . 11 ⊢ (∀𝑔𝑖𝑢 = 𝑓 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
114	113	eqcoms 2746	. . . . . . . . . 10 ⊢ (𝑓 = ∀𝑔𝑖𝑢 → ((¬ ∀𝑔𝑖𝑢 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ ∀𝑔𝑖𝑢 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ ∀𝑔𝑖𝑢 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
115	102, 114	syl5ibcom 244	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
116	115	rexlimdva 3212	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢 → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
117	67, 116	jaod 855	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
118	117	rexlimdva 3212	. . . . . 6 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
119		elndif 4059	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (Fmla‘𝑁) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
120	119	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
121	120	intnand 488	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
122	11, 121	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ω ∧ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
123	122	ex 412	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) → ¬ (𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))))
124	123	con2d 134	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → ((𝑢 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁)))
125	124	impl 455	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁))
126		elneeldif 3897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑏 ≠ 𝑣)
127	126	necomd 2998	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ (Fmla‘𝑁) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → 𝑣 ≠ 𝑏)
128	127	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → 𝑣 ≠ 𝑏)
129	128	neneqd 2947	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ 𝑣 = 𝑏)
130	129	olcd 870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → (¬ 𝑢 = 𝑎 ∨ ¬ 𝑣 = 𝑏))
131	130, 28	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩)
132	131	intnand 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (1o = 1o ∧ ⟨𝑢, 𝑣⟩ = ⟨𝑎, 𝑏⟩))
133	132, 40	sylnibr 328	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ∧ 𝑏 ∈ (Fmla‘𝑁)) → ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
134	133	ralrimiva 3107	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
135	134	ralrimivw 3108	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
136	135	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏))
137	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
138	137	ralrimivw 3108	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
139	138	ralrimivw 3108	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)
140	136, 139, 52	sylanbrc 582	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎))
141	125, 140	jca 511	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)))
142		eleq1 2826	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ (Fmla‘𝑁)))
143	142	notbid 317	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ↔ ¬ 𝑓 ∈ (Fmla‘𝑁)))
144		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ 𝑓 = (𝑎⊼𝑔𝑏)))
145	144	notbid 317	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
146	145	ralbidv 3120	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ↔ ∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏)))
147		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ 𝑓 = ∀𝑔𝑗𝑎))
148	147	notbid 317	. . . . . . . . . . . . . 14 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ¬ 𝑓 = ∀𝑔𝑗𝑎))
149	148	ralbidv 3120	. . . . . . . . . . . . 13 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎 ↔ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
150	146, 149	anbi12d 630	. . . . . . . . . . . 12 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
151	150	ralbidv 3120	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
152	143, 151	anbi12d 630	. . . . . . . . . 10 ⊢ ((𝑢⊼𝑔𝑣) = 𝑓 → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
153	152	eqcoms 2746	. . . . . . . . 9 ⊢ (𝑓 = (𝑢⊼𝑔𝑣) → ((¬ (𝑢⊼𝑔𝑣) ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ (𝑢⊼𝑔𝑣) = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ (𝑢⊼𝑔𝑣) = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
154	141, 153	syl5ibcom 244	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) → (𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
155	154	rexlimdva 3212	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣) → (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
156	155	rexlimdva 3212	. . . . . 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 33250	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑓 ∈ V) → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
159	158	elvd 3429	. . . . . . 7 ⊢ (𝑁 ∈ ω → (𝑓 ∈ (Fmla‘suc 𝑁) ↔ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
160	159	notbid 317	. . . . . 6 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ ¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))))
161		ioran 980	. . . . . . 7 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)))
162		ralnex 3163	. . . . . . . . . . . 12 ⊢ (∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ↔ ¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏))
163		ralnex 3163	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎 ↔ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)
164	162, 163	anbi12i 626	. . . . . . . . . . 11 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
165		ioran 980	. . . . . . . . . . 11 ⊢ (¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ (¬ ∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∧ ¬ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
166	164, 165	bitr4i 277	. . . . . . . . . 10 ⊢ ((∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
167	166	ralbii 3090	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
168		ralnex 3163	. . . . . . . . 9 ⊢ (∀𝑎 ∈ (Fmla‘𝑁) ¬ (∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎))
169	167, 168	bitr2i 275	. . . . . . . 8 ⊢ (¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎) ↔ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))
170	169	anbi2i 622	. . . . . . 7 ⊢ ((¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ¬ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
171	161, 170	bitri 274	. . . . . 6 ⊢ (¬ (𝑓 ∈ (Fmla‘𝑁) ∨ ∃𝑎 ∈ (Fmla‘𝑁)(∃𝑏 ∈ (Fmla‘𝑁)𝑓 = (𝑎⊼𝑔𝑏) ∨ ∃𝑗 ∈ ω 𝑓 = ∀𝑔𝑗𝑎)) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎)))
172	160, 171	bitrdi 286	. . . . 5 ⊢ (𝑁 ∈ ω → (¬ 𝑓 ∈ (Fmla‘suc 𝑁) ↔ (¬ 𝑓 ∈ (Fmla‘𝑁) ∧ ∀𝑎 ∈ (Fmla‘𝑁)(∀𝑏 ∈ (Fmla‘𝑁) ¬ 𝑓 = (𝑎⊼𝑔𝑏) ∧ ∀𝑗 ∈ ω ¬ 𝑓 = ∀𝑔𝑗𝑎))))
173	157, 172	sylibrd 258	. . . 4 ⊢ (𝑁 ∈ ω → ((∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑓 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑓 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑓 = (𝑢⊼𝑔𝑣)) → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
174	10, 173	syl5bi 241	. . 3 ⊢ (𝑁 ∈ ω → (𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} → ¬ 𝑓 ∈ (Fmla‘suc 𝑁)))
175	174	ralrimiv 3106	. 2 ⊢ (𝑁 ∈ ω → ∀𝑓 ∈ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))} ¬ 𝑓 ∈ (Fmla‘suc 𝑁))
176		disjr 4380	. 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 233	1 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∖ cdif 3880   ∩ cin 3882  ∅c0 4253  ⟨cop 4564  suc csuc 6253  ‘cfv 6418  (class class class)co 7255  ωcom 7687  1_oc1o 8260  2_oc2o 8261  ⊼_𝑔cgna 33196  ∀_𝑔cgol 33197  Fmlacfmla 33199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-2o 8268  df-map 8575  df-goel 33202  df-gona 33203  df-goal 33204  df-sat 33205  df-fmla 33207

This theorem is referenced by:  satffunlem2lem2  33268