satfvsucsuc

Description: The satisfaction predicate as function over wff codes of height ( N + 1 ) , expressed by the minimally necessary satisfaction predicates as function over wff codes of height N . (Contributed by AV, 21-Oct-2023)

	Ref	Expression
Hypotheses	satfvsucsuc.s	$⊢ S = M Sat E$
	satfvsucsuc.a	$⊢ A = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
	satfvsucsuc.b	$⊢ B = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
Assertion	satfvsucsuc	$⊢ (M \in V \land E \in W \land N \in ω) \to S (suc suc N) = S (suc N) \cup \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}$

Proof

Step	Hyp	Ref	Expression
1		satfvsucsuc.s	$⊢ S = M Sat E$
2		satfvsucsuc.a	$⊢ A = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
3		satfvsucsuc.b	$⊢ B = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
4		peano2	$⊢ N \in ω \to suc N \in ω$
5	1	satfvsuc	$⊢ (M \in V \land E \in W \land suc N \in ω) \to S (suc suc N) = S (suc N) \cup \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
6	4 5	syl3an3	$⊢ (M \in V \land E \in W \land N \in ω) \to S (suc suc N) = S (suc N) \cup \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
7		orc	$⊢ s \in S (suc N) \to (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
8	7	a1i	$⊢ (M \in V \land E \in W \land N \in ω) \to (s \in S (suc N) \to (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
9	2	eqeq2i	$⊢ y = A \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
10	9	anbi2i	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
11	10	rexbii	$⊢ \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
12	3	eqeq2i	$⊢ y = B \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
13	12	anbi2i	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
14	13	rexbii	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B) \leftrightarrow \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
15	11 14	orbi12i	$⊢ (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
16	15	rexbii	$⊢ \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
17	16	bicomi	$⊢ \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
18		3simpa	$⊢ (M \in V \land E \in W \land N \in ω) \to (M \in V \land E \in W)$
19	4	ancri	$⊢ N \in ω \to (suc N \in ω \land N \in ω)$
20	19	3ad2ant3	$⊢ (M \in V \land E \in W \land N \in ω) \to (suc N \in ω \land N \in ω)$
21	18 20	jca	$⊢ (M \in V \land E \in W \land N \in ω) \to ((M \in V \land E \in W) \land (suc N \in ω \land N \in ω))$
22		sssucid	$⊢ N \subseteq suc N$
23	22	a1i	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to N \subseteq suc N$
24	1	satfsschain	$⊢ ((M \in V \land E \in W) \land (suc N \in ω \land N \in ω)) \to (N \subseteq suc N \to S (N) \subseteq S (suc N))$
25	24	imp	$⊢ (((M \in V \land E \in W) \land (suc N \in ω \land N \in ω)) \land N \subseteq suc N) \to S (N) \subseteq S (suc N)$
26	21 23 25	syl2an2r	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to S (N) \subseteq S (suc N)$
27		undif	$⊢ S (N) \subseteq S (suc N) \leftrightarrow S (N) \cup (S (suc N) ∖ S (N)) = S (suc N)$
28	26 27	sylib	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to S (N) \cup (S (suc N) ∖ S (N)) = S (suc N)$
29	28	eqcomd	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to S (suc N) = S (N) \cup (S (suc N) ∖ S (N))$
30	29	rexeqdv	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow \exists u \in (S (N) \cup (S (suc N) ∖ S (N))) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
31		rexun	$⊢ \exists u \in (S (N) \cup (S (suc N) ∖ S (N))) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
32	30 31	bitrdi	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))))$
33	17 32	bitrid	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))))$
34		r19.43	$⊢ \exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
35	22	a1i	$⊢ (M \in V \land E \in W \land N \in ω) \to N \subseteq suc N$
36	21 35	jca	$⊢ (M \in V \land E \in W \land N \in ω) \to (((M \in V \land E \in W) \land (suc N \in ω \land N \in ω)) \land N \subseteq suc N)$
37	36 25	syl	$⊢ (M \in V \land E \in W \land N \in ω) \to S (N) \subseteq S (suc N)$
38	37	adantr	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to S (N) \subseteq S (suc N)$
39	38 27	sylib	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to S (N) \cup (S (suc N) ∖ S (N)) = S (suc N)$
40	39	eqcomd	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to S (suc N) = S (N) \cup (S (suc N) ∖ S (N))$
41	40	rexeqdv	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow \exists v \in (S (N) \cup (S (suc N) ∖ S (N))) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
42		rexun	$⊢ \exists v \in (S (N) \cup (S (suc N) ∖ S (N))) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
43	41 42	bitrdi	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
44	43	rexbidv	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
45	44	orbi1d	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to ((\exists u \in S (N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
46		r19.43	$⊢ \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \leftrightarrow (\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
47	46	orbi1i	$⊢ (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow ((\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
48		or32	$⊢ ((\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow ((\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
49		r19.43	$⊢ \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
50	49	bicomi	$⊢ (\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
51	50	orbi1i	$⊢ ((\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
52	48 51	bitri	$⊢ ((\exists u \in S (N) \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
53	47 52	bitri	$⊢ (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
54	45 53	bitrdi	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to ((\exists u \in S (N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists u \in S (N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
55	34 54	bitrid	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \leftrightarrow (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
56		animorr	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
57	1	satfvsuc	$⊢ (M \in V \land E \in W \land N \in ω) \to S (suc N) = S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
58	57	eleq2d	$⊢ (M \in V \land E \in W \land N \in ω) \to (s \in S (suc N) \leftrightarrow s \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}))$
59	58	adantr	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (s \in S (suc N) \leftrightarrow s \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}))$
60		eleq1	$⊢ s = ⟨x, y⟩ \to (s \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow ⟨x, y⟩ \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}))$
61	60	adantl	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (s \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow ⟨x, y⟩ \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}))$
62		elun	$⊢ ⟨x, y⟩ \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (⟨x, y⟩ \in S (N) \lor ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
63		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \leftrightarrow \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
64	63	orbi2i	$⊢ (⟨x, y⟩ \in S (N) \lor ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
65	62 64	bitri	$⊢ ⟨x, y⟩ \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
66	61 65	bitrdi	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (s \in (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
67	59 66	bitrd	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (s \in S (suc N) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
68	2	eqcomi	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) = A$
69	68	eqeq2i	$⊢ y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow y = A$
70	69	anbi2i	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)$
71	70	rexbii	$⊢ \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)$
72	3	eqcomi	$⊢ \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} = B$
73	72	eqeq2i	$⊢ y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow y = B$
74	73	anbi2i	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)$
75	74	rexbii	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)$
76	71 75	orbi12i	$⊢ (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
77	76	rexbii	$⊢ \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
78	77	a1i	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
79	78	orbi2d	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to ((⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))))$
80	67 79	bitrd	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (s \in S (suc N) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))))$
81	80	adantr	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (s \in S (suc N) \leftrightarrow (⟨x, y⟩ \in S (N) \lor \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))))$
82	56 81	mpbird	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to s \in S (suc N)$
83	82	orcd	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
84	83	ex	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
85		simplr	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to s = ⟨x, y⟩$
86		animorr	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
87	85 86	jca	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
88	87	olcd	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
89	88	ex	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
90	84 89	jaod	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to ((\exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
91	55 90	sylbid	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
92		simplr	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to s = ⟨x, y⟩$
93		orc	$⊢ \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
94	93	adantl	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
95	92 94	jca	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
96	95	olcd	$⊢ (((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \land \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
97	96	ex	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
98	91 97	jaod	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to ((\exists u \in S (N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
99	33 98	sylbid	$⊢ ((M \in V \land E \in W \land N \in ω) \land s = ⟨x, y⟩) \to (\exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
100	99	expimpd	$⊢ (M \in V \land E \in W \land N \in ω) \to ((s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
101	100	2eximdv	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to \exists x \exists y (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
102		19.45v	$⊢ \exists y (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))) \leftrightarrow (s \in S (suc N) \lor \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
103	102	exbii	$⊢ \exists x \exists y (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))) \leftrightarrow \exists x (s \in S (suc N) \lor \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
104		19.45v	$⊢ \exists x (s \in S (suc N) \lor \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
105	103 104	bitri	$⊢ \exists x \exists y (s \in S (suc N) \lor (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
106	101 105	imbitrdi	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
107	8 106	jaod	$⊢ (M \in V \land E \in W \land N \in ω) \to ((s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))) \to (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
108		difss	$⊢ S (suc N) ∖ S (N) \subseteq S (suc N)$
109		ssrexv	$⊢ S (suc N) ∖ S (N) \subseteq S (suc N) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
110	108 109	ax-mp	$⊢ \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B))$
111	110	a1i	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)))$
112	111 16	imbitrdi	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \to \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
113		ssrexv	$⊢ S (N) \subseteq S (suc N) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \to \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
114	37 113	syl	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \to \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))$
115	10	2rexbii	$⊢ \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
116	114 115	imbitrdi	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \to \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
117	116	imp	$⊢ ((M \in V \land E \in W \land N \in ω) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
118		ssrexv	$⊢ S (suc N) ∖ S (N) \subseteq S (suc N) \to (\exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
119	108 118	ax-mp	$⊢ \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
120	119	reximi	$⊢ \exists u \in S (suc N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to \exists u \in S (suc N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
121	117 120	syl	$⊢ ((M \in V \land E \in W \land N \in ω) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to \exists u \in S (suc N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
122	121	orcd	$⊢ ((M \in V \land E \in W \land N \in ω) \land \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to (\exists u \in S (suc N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists u \in S (suc N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
123	122	ex	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \to (\exists u \in S (suc N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists u \in S (suc N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
124		r19.43	$⊢ \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists u \in S (suc N) \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists u \in S (suc N) \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
125	123 124	syl6ibr	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \to \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
126	112 125	jaod	$⊢ (M \in V \land E \in W \land N \in ω) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \to \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
127	126	anim2d	$⊢ (M \in V \land E \in W \land N \in ω) \to ((s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))) \to (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
128	127	2eximdv	$⊢ (M \in V \land E \in W \land N \in ω) \to (\exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))) \to \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
129	128	orim2d	$⊢ (M \in V \land E \in W \land N \in ω) \to ((s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))) \to (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))))$
130	107 129	impbid	$⊢ (M \in V \land E \in W \land N \in ω) \to ((s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))))$
131		elun	$⊢ s \in (S (suc N) \cup \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (s \in S (suc N) \lor s \in \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
132		elopab	$⊢ s \in \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \leftrightarrow \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
133	132	orbi2i	$⊢ (s \in S (suc N) \lor s \in \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
134	131 133	bitri	$⊢ s \in (S (suc N) \cup \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
135		elun	$⊢ s \in (S (suc N) \cup \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}) \leftrightarrow (s \in S (suc N) \lor s \in \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\})$
136		elopab	$⊢ s \in \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} \leftrightarrow \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)))$
137	136	orbi2i	$⊢ (s \in S (suc N) \lor s \in \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
138	135 137	bitri	$⊢ s \in (S (suc N) \cup \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}) \leftrightarrow (s \in S (suc N) \lor \exists x \exists y (s = ⟨x, y⟩ \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))))$
139	130 134 138	3bitr4g	$⊢ (M \in V \land E \in W \land N \in ω) \to (s \in (S (suc N) \cup \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow s \in (S (suc N) \cup \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}))$
140	139	eqrdv	$⊢ (M \in V \land E \in W \land N \in ω) \to S (suc N) \cup \{⟨x, y⟩ \| \exists u \in S (suc N) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = S (suc N) \cup \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}$
141	6 140	eqtrd	$⊢ (M \in V \land E \in W \land N \in ω) \to S (suc suc N) = S (suc N) \cup \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\}$

Metamath Proof Explorer

Theorem satfvsucsuc

Proof