fmlasucdisj

Description: The valid Godel formulas of height ( N + 1 ) is disjoint with the difference ( ( Fmlasuc suc N ) \ ( Fmlasuc N ) ) , 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 ( N + 1 ) . (Contributed by AV, 20-Oct-2023)

		Ref	Expression
	Assertion	fmlasucdisj	$⊢ N \in ω \to Fmla (suc N) \cap \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ f \in V$
2		eqeq1	$⊢ x = f \to (x = u ⊼_{𝑔} v \leftrightarrow f = u ⊼_{𝑔} v)$
3	2	rexbidv	$⊢ x = f \to (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \leftrightarrow \exists v \in Fmla (suc N) f = u ⊼_{𝑔} v)$
4		eqeq1	$⊢ x = f \to (x = [\forall_{𝑔} i u] \leftrightarrow f = [\forall_{𝑔} i u])$
5	4	rexbidv	$⊢ x = f \to (\exists i \in ω x = [\forall_{𝑔} i u] \leftrightarrow \exists i \in ω f = [\forall_{𝑔} i u])$
6	3 5	orbi12d	$⊢ x = f \to ((\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]))$
7	6	rexbidv	$⊢ x = f \to (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow \exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]))$
8	2	2rexbidv	$⊢ x = f \to (\exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v \leftrightarrow \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v)$
9	7 8	orbi12d	$⊢ x = f \to ((\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v) \leftrightarrow (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v))$
10	1 9	elab	$⊢ f \in \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} \leftrightarrow (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v)$
11		gonar	$⊢ (N \in ω \land u ⊼_{𝑔} v \in Fmla (N)) \to (u \in Fmla (N) \land v \in Fmla (N))$
12		elndif	$⊢ u \in Fmla (N) \to \neg u \in (Fmla (suc N) ∖ Fmla (N))$
13	12	adantr	$⊢ (u \in Fmla (N) \land v \in Fmla (N)) \to \neg u \in (Fmla (suc N) ∖ Fmla (N))$
14	13	intnanrd	$⊢ (u \in Fmla (N) \land v \in Fmla (N)) \to \neg (u \in (Fmla (suc N) ∖ Fmla (N)) \land v \in Fmla (suc N))$
15	11 14	syl	$⊢ (N \in ω \land u ⊼_{𝑔} v \in Fmla (N)) \to \neg (u \in (Fmla (suc N) ∖ Fmla (N)) \land v \in Fmla (suc N))$
16	15	ex	$⊢ N \in ω \to (u ⊼_{𝑔} v \in Fmla (N) \to \neg (u \in (Fmla (suc N) ∖ Fmla (N)) \land v \in Fmla (suc N)))$
17	16	con2d	$⊢ N \in ω \to ((u \in (Fmla (suc N) ∖ Fmla (N)) \land v \in Fmla (suc N)) \to \neg u ⊼_{𝑔} v \in Fmla (N))$
18	17	impl	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to \neg u ⊼_{𝑔} v \in Fmla (N)$
19		elneeldif	$⊢ (a \in Fmla (N) \land u \in (Fmla (suc N) ∖ Fmla (N))) \to a \neq u$
20	19	necomd	$⊢ (a \in Fmla (N) \land u \in (Fmla (suc N) ∖ Fmla (N))) \to u \neq a$
21	20	ancoms	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to u \neq a$
22	21	neneqd	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \neg u = a$
23	22	orcd	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to (\neg u = a \lor \neg v = b)$
24		ianor	$⊢ \neg (u = a \land v = b) \leftrightarrow (\neg u = a \lor \neg v = b)$
25		vex	$⊢ u \in V$
26		vex	$⊢ v \in V$
27	25 26	opth	$⊢ ⟨u, v⟩ = ⟨a, b⟩ \leftrightarrow (u = a \land v = b)$
28	24 27	xchnxbir	$⊢ \neg ⟨u, v⟩ = ⟨a, b⟩ \leftrightarrow (\neg u = a \lor \neg v = b)$
29	23 28	sylibr	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \neg ⟨u, v⟩ = ⟨a, b⟩$
30	29	olcd	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to (\neg 1_{𝑜} = 1_{𝑜} \lor \neg ⟨u, v⟩ = ⟨a, b⟩)$
31		ianor	$⊢ \neg (1_{𝑜} = 1_{𝑜} \land ⟨u, v⟩ = ⟨a, b⟩) \leftrightarrow (\neg 1_{𝑜} = 1_{𝑜} \lor \neg ⟨u, v⟩ = ⟨a, b⟩)$
32		gonafv	$⊢ (u \in V \land v \in V) \to u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
33	32	el2v	$⊢ u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
34		gonafv	$⊢ (a \in V \land b \in V) \to a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
35	34	el2v	$⊢ a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
36	33 35	eqeq12i	$⊢ u ⊼_{𝑔} v = a ⊼_{𝑔} b \leftrightarrow ⟨1_{𝑜}, ⟨u, v⟩⟩ = ⟨1_{𝑜}, ⟨a, b⟩⟩$
37		1oex	$⊢ 1_{𝑜} \in V$
38		opex	$⊢ ⟨u, v⟩ \in V$
39	37 38	opth	$⊢ ⟨1_{𝑜}, ⟨u, v⟩⟩ = ⟨1_{𝑜}, ⟨a, b⟩⟩ \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨u, v⟩ = ⟨a, b⟩)$
40	36 39	bitri	$⊢ u ⊼_{𝑔} v = a ⊼_{𝑔} b \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨u, v⟩ = ⟨a, b⟩)$
41	31 40	xchnxbir	$⊢ \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \leftrightarrow (\neg 1_{𝑜} = 1_{𝑜} \lor \neg ⟨u, v⟩ = ⟨a, b⟩)$
42	30 41	sylibr	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
43	42	ralrimivw	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
44	43	ralrimiva	$⊢ u \in (Fmla (suc N) ∖ Fmla (N)) \to \forall a \in Fmla (N) \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
45	44	adantl	$⊢ (N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \to \forall a \in Fmla (N) \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
46	45	adantr	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to \forall a \in Fmla (N) \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
47		gonanegoal	$⊢ u ⊼_{𝑔} v \neq [\forall_{𝑔} j a]$
48	47	neii	$⊢ \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
49	48	a1i	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
50	49	ralrimivw	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
51	50	ralrimivw	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to \forall a \in Fmla (N) \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
52		r19.26	$⊢ \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]) \leftrightarrow (\forall a \in Fmla (N) \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall a \in Fmla (N) \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])$
53	46 51 52	sylanbrc	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])$
54	18 53	jca	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to (\neg u ⊼_{𝑔} v \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]))$
55		eleq1	$⊢ f = u ⊼_{𝑔} v \to (f \in Fmla (N) \leftrightarrow u ⊼_{𝑔} v \in Fmla (N))$
56	55	notbid	$⊢ f = u ⊼_{𝑔} v \to (\neg f \in Fmla (N) \leftrightarrow \neg u ⊼_{𝑔} v \in Fmla (N))$
57		eqeq1	$⊢ f = u ⊼_{𝑔} v \to (f = a ⊼_{𝑔} b \leftrightarrow u ⊼_{𝑔} v = a ⊼_{𝑔} b)$
58	57	notbid	$⊢ f = u ⊼_{𝑔} v \to (\neg f = a ⊼_{𝑔} b \leftrightarrow \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b)$
59	58	ralbidv	$⊢ f = u ⊼_{𝑔} v \to (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \leftrightarrow \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b)$
60		eqeq1	$⊢ f = u ⊼_{𝑔} v \to (f = [\forall_{𝑔} j a] \leftrightarrow u ⊼_{𝑔} v = [\forall_{𝑔} j a])$
61	60	notbid	$⊢ f = u ⊼_{𝑔} v \to (\neg f = [\forall_{𝑔} j a] \leftrightarrow \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])$
62	61	ralbidv	$⊢ f = u ⊼_{𝑔} v \to (\forall j \in ω \neg f = [\forall_{𝑔} j a] \leftrightarrow \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])$
63	59 62	anbi12d	$⊢ f = u ⊼_{𝑔} v \to ((\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]) \leftrightarrow (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]))$
64	63	ralbidv	$⊢ f = u ⊼_{𝑔} v \to (\forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]) \leftrightarrow \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]))$
65	56 64	anbi12d	$⊢ f = u ⊼_{𝑔} v \to ((\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])) \leftrightarrow (\neg u ⊼_{𝑔} v \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])))$
66	54 65	syl5ibrcom	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land v \in Fmla (suc N)) \to (f = u ⊼_{𝑔} v \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
67	66	rexlimdva	$⊢ (N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \to (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
68		goalr	$⊢ (N \in ω \land [\forall_{𝑔} i u] \in Fmla (N)) \to u \in Fmla (N)$
69	68 12	syl	$⊢ (N \in ω \land [\forall_{𝑔} i u] \in Fmla (N)) \to \neg u \in (Fmla (suc N) ∖ Fmla (N))$
70	69	ex	$⊢ N \in ω \to ([\forall_{𝑔} i u] \in Fmla (N) \to \neg u \in (Fmla (suc N) ∖ Fmla (N)))$
71	70	con2d	$⊢ N \in ω \to (u \in (Fmla (suc N) ∖ Fmla (N)) \to \neg [\forall_{𝑔} i u] \in Fmla (N))$
72	71	imp	$⊢ (N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \to \neg [\forall_{𝑔} i u] \in Fmla (N)$
73	72	adantr	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to \neg [\forall_{𝑔} i u] \in Fmla (N)$
74		gonanegoal	$⊢ a ⊼_{𝑔} b \neq [\forall_{𝑔} i u]$
75	74	nesymi	$⊢ \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b$
76	75	a1i	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b$
77	76	ralrimivw	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to \forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b$
78	77	ralrimivw	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to \forall a \in Fmla (N) \forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b$
79	22	olcd	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to (\neg i = j \lor \neg u = a)$
80		ianor	$⊢ \neg (i = j \land u = a) \leftrightarrow (\neg i = j \lor \neg u = a)$
81		vex	$⊢ i \in V$
82	81 25	opth	$⊢ ⟨i, u⟩ = ⟨j, a⟩ \leftrightarrow (i = j \land u = a)$
83	80 82	xchnxbir	$⊢ \neg ⟨i, u⟩ = ⟨j, a⟩ \leftrightarrow (\neg i = j \lor \neg u = a)$
84	79 83	sylibr	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \neg ⟨i, u⟩ = ⟨j, a⟩$
85	84	olcd	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to (\neg 2_{𝑜} = 2_{𝑜} \lor \neg ⟨i, u⟩ = ⟨j, a⟩)$
86		ianor	$⊢ \neg (2_{𝑜} = 2_{𝑜} \land ⟨i, u⟩ = ⟨j, a⟩) \leftrightarrow (\neg 2_{𝑜} = 2_{𝑜} \lor \neg ⟨i, u⟩ = ⟨j, a⟩)$
87		2oex	$⊢ 2_{𝑜} \in V$
88		opex	$⊢ ⟨i, u⟩ \in V$
89	87 88	opth	$⊢ ⟨2_{𝑜}, ⟨i, u⟩⟩ = ⟨2_{𝑜}, ⟨j, a⟩⟩ \leftrightarrow (2_{𝑜} = 2_{𝑜} \land ⟨i, u⟩ = ⟨j, a⟩)$
90	86 89	xchnxbir	$⊢ \neg ⟨2_{𝑜}, ⟨i, u⟩⟩ = ⟨2_{𝑜}, ⟨j, a⟩⟩ \leftrightarrow (\neg 2_{𝑜} = 2_{𝑜} \lor \neg ⟨i, u⟩ = ⟨j, a⟩)$
91		df-goal	$⊢ [\forall_{𝑔} i u] = ⟨2_{𝑜}, ⟨i, u⟩⟩$
92		df-goal	$⊢ [\forall_{𝑔} j a] = ⟨2_{𝑜}, ⟨j, a⟩⟩$
93	91 92	eqeq12i	$⊢ [\forall_{𝑔} i u] = [\forall_{𝑔} j a] \leftrightarrow ⟨2_{𝑜}, ⟨i, u⟩⟩ = ⟨2_{𝑜}, ⟨j, a⟩⟩$
94	90 93	xchnxbir	$⊢ \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a] \leftrightarrow (\neg 2_{𝑜} = 2_{𝑜} \lor \neg ⟨i, u⟩ = ⟨j, a⟩)$
95	85 94	sylibr	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]$
96	95	ralrimivw	$⊢ (u \in (Fmla (suc N) ∖ Fmla (N)) \land a \in Fmla (N)) \to \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]$
97	96	ralrimiva	$⊢ u \in (Fmla (suc N) ∖ Fmla (N)) \to \forall a \in Fmla (N) \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]$
98	97	adantl	$⊢ (N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \to \forall a \in Fmla (N) \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]$
99	98	adantr	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to \forall a \in Fmla (N) \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]$
100		r19.26	$⊢ \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]) \leftrightarrow (\forall a \in Fmla (N) \forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall a \in Fmla (N) \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a])$
101	78 99 100	sylanbrc	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a])$
102	73 101	jca	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to (\neg [\forall_{𝑔} i u] \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]))$
103		eleq1	$⊢ [\forall_{𝑔} i u] = f \to ([\forall_{𝑔} i u] \in Fmla (N) \leftrightarrow f \in Fmla (N))$
104	103	notbid	$⊢ [\forall_{𝑔} i u] = f \to (\neg [\forall_{𝑔} i u] \in Fmla (N) \leftrightarrow \neg f \in Fmla (N))$
105		eqeq1	$⊢ [\forall_{𝑔} i u] = f \to ([\forall_{𝑔} i u] = a ⊼_{𝑔} b \leftrightarrow f = a ⊼_{𝑔} b)$
106	105	notbid	$⊢ [\forall_{𝑔} i u] = f \to (\neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \leftrightarrow \neg f = a ⊼_{𝑔} b)$
107	106	ralbidv	$⊢ [\forall_{𝑔} i u] = f \to (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \leftrightarrow \forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b)$
108		eqeq1	$⊢ [\forall_{𝑔} i u] = f \to ([\forall_{𝑔} i u] = [\forall_{𝑔} j a] \leftrightarrow f = [\forall_{𝑔} j a])$
109	108	notbid	$⊢ [\forall_{𝑔} i u] = f \to (\neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a] \leftrightarrow \neg f = [\forall_{𝑔} j a])$
110	109	ralbidv	$⊢ [\forall_{𝑔} i u] = f \to (\forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a] \leftrightarrow \forall j \in ω \neg f = [\forall_{𝑔} j a])$
111	107 110	anbi12d	$⊢ [\forall_{𝑔} i u] = f \to ((\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]) \leftrightarrow (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]))$
112	111	ralbidv	$⊢ [\forall_{𝑔} i u] = f \to (\forall a \in Fmla (N) (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a]) \leftrightarrow \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]))$
113	104 112	anbi12d	$⊢ [\forall_{𝑔} i u] = f \to ((\neg [\forall_{𝑔} i u] \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
114	113	eqcoms	$⊢ f = [\forall_{𝑔} i u] \to ((\neg [\forall_{𝑔} i u] \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg [\forall_{𝑔} i u] = a ⊼_{𝑔} b \land \forall j \in ω \neg [\forall_{𝑔} i u] = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
115	102 114	syl5ibcom	$⊢ ((N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \land i \in ω) \to (f = [\forall_{𝑔} i u] \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
116	115	rexlimdva	$⊢ (N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \to (\exists i \in ω f = [\forall_{𝑔} i u] \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
117	67 116	jaod	$⊢ (N \in ω \land u \in (Fmla (suc N) ∖ Fmla (N))) \to ((\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]) \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
118	117	rexlimdva	$⊢ N \in ω \to (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]) \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
119		elndif	$⊢ v \in Fmla (N) \to \neg v \in (Fmla (suc N) ∖ Fmla (N))$
120	119	adantl	$⊢ (u \in Fmla (N) \land v \in Fmla (N)) \to \neg v \in (Fmla (suc N) ∖ Fmla (N))$
121	120	intnand	$⊢ (u \in Fmla (N) \land v \in Fmla (N)) \to \neg (u \in Fmla (N) \land v \in (Fmla (suc N) ∖ Fmla (N)))$
122	11 121	syl	$⊢ (N \in ω \land u ⊼_{𝑔} v \in Fmla (N)) \to \neg (u \in Fmla (N) \land v \in (Fmla (suc N) ∖ Fmla (N)))$
123	122	ex	$⊢ N \in ω \to (u ⊼_{𝑔} v \in Fmla (N) \to \neg (u \in Fmla (N) \land v \in (Fmla (suc N) ∖ Fmla (N))))$
124	123	con2d	$⊢ N \in ω \to ((u \in Fmla (N) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \neg u ⊼_{𝑔} v \in Fmla (N))$
125	124	impl	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \neg u ⊼_{𝑔} v \in Fmla (N)$
126		elneeldif	$⊢ (b \in Fmla (N) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to b \neq v$
127	126	necomd	$⊢ (b \in Fmla (N) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to v \neq b$
128	127	ancoms	$⊢ (v \in (Fmla (suc N) ∖ Fmla (N)) \land b \in Fmla (N)) \to v \neq b$
129	128	neneqd	$⊢ (v \in (Fmla (suc N) ∖ Fmla (N)) \land b \in Fmla (N)) \to \neg v = b$
130	129	olcd	$⊢ (v \in (Fmla (suc N) ∖ Fmla (N)) \land b \in Fmla (N)) \to (\neg u = a \lor \neg v = b)$
131	130 28	sylibr	$⊢ (v \in (Fmla (suc N) ∖ Fmla (N)) \land b \in Fmla (N)) \to \neg ⟨u, v⟩ = ⟨a, b⟩$
132	131	intnand	$⊢ (v \in (Fmla (suc N) ∖ Fmla (N)) \land b \in Fmla (N)) \to \neg (1_{𝑜} = 1_{𝑜} \land ⟨u, v⟩ = ⟨a, b⟩)$
133	132 40	sylnibr	$⊢ (v \in (Fmla (suc N) ∖ Fmla (N)) \land b \in Fmla (N)) \to \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
134	133	ralrimiva	$⊢ v \in (Fmla (suc N) ∖ Fmla (N)) \to \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
135	134	ralrimivw	$⊢ v \in (Fmla (suc N) ∖ Fmla (N)) \to \forall a \in Fmla (N) \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
136	135	adantl	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \forall a \in Fmla (N) \forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b$
137	48	a1i	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
138	137	ralrimivw	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
139	138	ralrimivw	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \forall a \in Fmla (N) \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]$
140	136 139 52	sylanbrc	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])$
141	125 140	jca	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to (\neg u ⊼_{𝑔} v \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]))$
142		eleq1	$⊢ u ⊼_{𝑔} v = f \to (u ⊼_{𝑔} v \in Fmla (N) \leftrightarrow f \in Fmla (N))$
143	142	notbid	$⊢ u ⊼_{𝑔} v = f \to (\neg u ⊼_{𝑔} v \in Fmla (N) \leftrightarrow \neg f \in Fmla (N))$
144		eqeq1	$⊢ u ⊼_{𝑔} v = f \to (u ⊼_{𝑔} v = a ⊼_{𝑔} b \leftrightarrow f = a ⊼_{𝑔} b)$
145	144	notbid	$⊢ u ⊼_{𝑔} v = f \to (\neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \leftrightarrow \neg f = a ⊼_{𝑔} b)$
146	145	ralbidv	$⊢ u ⊼_{𝑔} v = f \to (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \leftrightarrow \forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b)$
147		eqeq1	$⊢ u ⊼_{𝑔} v = f \to (u ⊼_{𝑔} v = [\forall_{𝑔} j a] \leftrightarrow f = [\forall_{𝑔} j a])$
148	147	notbid	$⊢ u ⊼_{𝑔} v = f \to (\neg u ⊼_{𝑔} v = [\forall_{𝑔} j a] \leftrightarrow \neg f = [\forall_{𝑔} j a])$
149	148	ralbidv	$⊢ u ⊼_{𝑔} v = f \to (\forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a] \leftrightarrow \forall j \in ω \neg f = [\forall_{𝑔} j a])$
150	146 149	anbi12d	$⊢ u ⊼_{𝑔} v = f \to ((\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]) \leftrightarrow (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]))$
151	150	ralbidv	$⊢ u ⊼_{𝑔} v = f \to (\forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a]) \leftrightarrow \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]))$
152	143 151	anbi12d	$⊢ u ⊼_{𝑔} v = f \to ((\neg u ⊼_{𝑔} v \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
153	152	eqcoms	$⊢ f = u ⊼_{𝑔} v \to ((\neg u ⊼_{𝑔} v \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg u ⊼_{𝑔} v = a ⊼_{𝑔} b \land \forall j \in ω \neg u ⊼_{𝑔} v = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
154	141 153	syl5ibcom	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in (Fmla (suc N) ∖ Fmla (N))) \to (f = u ⊼_{𝑔} v \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
155	154	rexlimdva	$⊢ (N \in ω \land u \in Fmla (N)) \to (\exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
156	155	rexlimdva	$⊢ N \in ω \to (\exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
157	118 156	jaod	$⊢ N \in ω \to ((\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v) \to (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
158		isfmlasuc	$⊢ (N \in ω \land f \in V) \to (f \in Fmla (suc N) \leftrightarrow (f \in Fmla (N) \lor \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])))$
159	158	elvd	$⊢ N \in ω \to (f \in Fmla (suc N) \leftrightarrow (f \in Fmla (N) \lor \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])))$
160	159	notbid	$⊢ N \in ω \to (\neg f \in Fmla (suc N) \leftrightarrow \neg (f \in Fmla (N) \lor \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])))$
161		ioran	$⊢ \neg (f \in Fmla (N) \lor \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \neg \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a]))$
162		ralnex	$⊢ \forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \leftrightarrow \neg \exists b \in Fmla (N) f = a ⊼_{𝑔} b$
163		ralnex	$⊢ \forall j \in ω \neg f = [\forall_{𝑔} j a] \leftrightarrow \neg \exists j \in ω f = [\forall_{𝑔} j a]$
164	162 163	anbi12i	$⊢ (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]) \leftrightarrow (\neg \exists b \in Fmla (N) f = a ⊼_{𝑔} b \land \neg \exists j \in ω f = [\forall_{𝑔} j a])$
165		ioran	$⊢ \neg (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a]) \leftrightarrow (\neg \exists b \in Fmla (N) f = a ⊼_{𝑔} b \land \neg \exists j \in ω f = [\forall_{𝑔} j a])$
166	164 165	bitr4i	$⊢ (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]) \leftrightarrow \neg (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])$
167	166	ralbii	$⊢ \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]) \leftrightarrow \forall a \in Fmla (N) \neg (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])$
168		ralnex	$⊢ \forall a \in Fmla (N) \neg (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a]) \leftrightarrow \neg \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])$
169	167 168	bitr2i	$⊢ \neg \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a]) \leftrightarrow \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])$
170	169	anbi2i	$⊢ (\neg f \in Fmla (N) \land \neg \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]))$
171	161 170	bitri	$⊢ \neg (f \in Fmla (N) \lor \exists a \in Fmla (N) (\exists b \in Fmla (N) f = a ⊼_{𝑔} b \lor \exists j \in ω f = [\forall_{𝑔} j a])) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a]))$
172	160 171	bitrdi	$⊢ N \in ω \to (\neg f \in Fmla (suc N) \leftrightarrow (\neg f \in Fmla (N) \land \forall a \in Fmla (N) (\forall b \in Fmla (N) \neg f = a ⊼_{𝑔} b \land \forall j \in ω \neg f = [\forall_{𝑔} j a])))$
173	157 172	sylibrd	$⊢ N \in ω \to ((\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) f = u ⊼_{𝑔} v \lor \exists i \in ω f = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) f = u ⊼_{𝑔} v) \to \neg f \in Fmla (suc N))$
174	10 173	syl5bi	$⊢ N \in ω \to (f \in \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} \to \neg f \in Fmla (suc N))$
175	174	ralrimiv	$⊢ N \in ω \to \forall f \in \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} \neg f \in Fmla (suc N)$
176		disjr	$⊢ Fmla (suc N) \cap \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} = \emptyset \leftrightarrow \forall f \in \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} \neg f \in Fmla (suc N)$
177	175 176	sylibr	$⊢ N \in ω \to Fmla (suc N) \cap \{x \| (\exists u \in (Fmla (suc N) ∖ Fmla (N)) (\exists v \in Fmla (suc N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \lor \exists u \in Fmla (N) \exists v \in (Fmla (suc N) ∖ Fmla (N)) x = u ⊼_{𝑔} v)\} = \emptyset$

Metamath Proof Explorer

Theorem fmlasucdisj

Proof