satffunlem2lem1

	Ref	Expression
Hypotheses	satffunlem2lem1.s	$⊢ S = M Sat E$
	satffunlem2lem1.a	$⊢ A = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
	satffunlem2lem1.b	$⊢ B = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
Assertion	satffunlem2lem1	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to Fun \{⟨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		satffunlem2lem1.s	$⊢ S = M Sat E$
2		satffunlem2lem1.a	$⊢ A = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
3		satffunlem2lem1.b	$⊢ B = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
4		simpl	$⊢ (u = s \land v = r) \to u = s$
5	4	fveq2d	$⊢ (u = s \land v = r) \to 1^{st} (u) = 1^{st} (s)$
6		simpr	$⊢ (u = s \land v = r) \to v = r$
7	6	fveq2d	$⊢ (u = s \land v = r) \to 1^{st} (v) = 1^{st} (r)$
8	5 7	oveq12d	$⊢ (u = s \land v = r) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r)$
9	8	eqeq2d	$⊢ (u = s \land v = r) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r))$
10	4	fveq2d	$⊢ (u = s \land v = r) \to 2^{nd} (u) = 2^{nd} (s)$
11	6	fveq2d	$⊢ (u = s \land v = r) \to 2^{nd} (v) = 2^{nd} (r)$
12	10 11	ineq12d	$⊢ (u = s \land v = r) \to 2^{nd} (u) \cap 2^{nd} (v) = 2^{nd} (s) \cap 2^{nd} (r)$
13	12	difeq2d	$⊢ (u = s \land v = r) \to (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))$
14	2 13	eqtrid	$⊢ (u = s \land v = r) \to A = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))$
15	14	eqeq2d	$⊢ (u = s \land v = r) \to (y = A \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
16	9 15	anbi12d	$⊢ (u = s \land v = r) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
17	16	cbvrexdva	$⊢ u = s \to (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow \exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
18		simpr	$⊢ (u = s \land i = j) \to i = j$
19		fveq2	$⊢ u = s \to 1^{st} (u) = 1^{st} (s)$
20	19	adantr	$⊢ (u = s \land i = j) \to 1^{st} (u) = 1^{st} (s)$
21	18 20	goaleq12d	$⊢ (u = s \land i = j) \to [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)]$
22	21	eqeq2d	$⊢ (u = s \land i = j) \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} j 1^{st} (s)])$
23	3	eqeq2i	$⊢ y = B \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
24		opeq1	$⊢ i = j \to ⟨i, z⟩ = ⟨j, z⟩$
25	24	sneqd	$⊢ i = j \to \{⟨i, z⟩\} = \{⟨j, z⟩\}$
26		sneq	$⊢ i = j \to \{i\} = \{j\}$
27	26	difeq2d	$⊢ i = j \to ω ∖ \{i\} = ω ∖ \{j\}$
28	27	reseq2d	$⊢ i = j \to {a ↾}_{(ω ∖ \{i\})} = {a ↾}_{(ω ∖ \{j\})}$
29	25 28	uneq12d	$⊢ i = j \to \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) = \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})})$
30	29	adantl	$⊢ (u = s \land i = j) \to \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) = \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})})$
31		fveq2	$⊢ u = s \to 2^{nd} (u) = 2^{nd} (s)$
32	31	adantr	$⊢ (u = s \land i = j) \to 2^{nd} (u) = 2^{nd} (s)$
33	30 32	eleq12d	$⊢ (u = s \land i = j) \to (\{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u) \leftrightarrow \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s))$
34	33	ralbidv	$⊢ (u = s \land i = j) \to (\forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u) \leftrightarrow \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s))$
35	34	rabbidv	$⊢ (u = s \land i = j) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}$
36	35	eqeq2d	$⊢ (u = s \land i = j) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})$
37	23 36	bitrid	$⊢ (u = s \land i = j) \to (y = B \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})$
38	22 37	anbi12d	$⊢ (u = s \land i = j) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = B) \leftrightarrow (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}))$
39	38	cbvrexdva	$⊢ u = s \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B) \leftrightarrow \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}))$
40	17 39	orbi12d	$⊢ u = s \to ((\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 r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})))$
41	40	cbvrexvw	$⊢ \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)) \leftrightarrow \exists s \in (S (suc N) ∖ S (N)) (\exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}))$
42		fveq2	$⊢ v = r \to 1^{st} (v) = 1^{st} (r)$
43	19 42	oveqan12d	$⊢ (u = s \land v = r) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r)$
44	43	eqeq2d	$⊢ (u = s \land v = r) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r))$
45	2	eqeq2i	$⊢ y = A \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
46		fveq2	$⊢ v = r \to 2^{nd} (v) = 2^{nd} (r)$
47	31 46	ineqan12d	$⊢ (u = s \land v = r) \to 2^{nd} (u) \cap 2^{nd} (v) = 2^{nd} (s) \cap 2^{nd} (r)$
48	47	difeq2d	$⊢ (u = s \land v = r) \to (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))$
49	48	eqeq2d	$⊢ (u = s \land v = r) \to (y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
50	45 49	bitrid	$⊢ (u = s \land v = r) \to (y = A \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
51	44 50	anbi12d	$⊢ (u = s \land v = r) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
52	51	cbvrexdva	$⊢ u = s \to (\exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow \exists r \in (S (suc N) ∖ S (N)) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
53	52	cbvrexvw	$⊢ \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 s \in S (N) \exists r \in (S (suc N) ∖ S (N)) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
54	41 53	orbi12i	$⊢ (\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 s \in (S (suc N) ∖ S (N)) (\exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})) \lor \exists s \in S (N) \exists r \in (S (suc N) ∖ S (N)) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
55		simp-5l	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \to Fun S (suc N)$
56		eldifi	$⊢ s \in (S (suc N) ∖ S (N)) \to s \in S (suc N)$
57	56	adantl	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \to s \in S (suc N)$
58	57	anim1i	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \to (s \in S (suc N) \land r \in S (suc N))$
59	58	ad2antrr	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \to (s \in S (suc N) \land r \in S (suc N))$
60		eldifi	$⊢ u \in (S (suc N) ∖ S (N)) \to u \in S (suc N)$
61	60	adantl	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to u \in S (suc N)$
62	61	anim1i	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \to (u \in S (suc N) \land v \in S (suc N))$
63	55 59 62	3jca	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \to (Fun S (suc N) \land (s \in S (suc N) \land r \in S (suc N)) \land (u \in S (suc N) \land v \in S (suc N)))$
64		id	$⊢ (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
65	2	eqeq2i	$⊢ w = A \leftrightarrow w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
66	65	biimpi	$⊢ w = A \to w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
67	66	anim2i	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
68		satffunlem	$⊢ ((Fun S (suc N) \land (s \in S (suc N) \land r \in S (suc N)) \land (u \in S (suc N) \land v \in S (suc N))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to y = w$
69	63 64 67 68	syl3an	$⊢ ((((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w$
70	69	3exp	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
71	70	com23	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
72	71	rexlimdva	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
73		eqeq1	$⊢ x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = [\forall_{𝑔} i 1^{st} (u)])$
74		fvex	$⊢ 1^{st} (s) \in V$
75		fvex	$⊢ 1^{st} (r) \in V$
76		gonafv	$⊢ (1^{st} (s) \in V \land 1^{st} (r) \in V) \to 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
77	74 75 76	mp2an	$⊢ 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
78		df-goal	$⊢ [\forall_{𝑔} i 1^{st} (u)] = ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩$
79	77 78	eqeq12i	$⊢ 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩ = ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩$
80		1oex	$⊢ 1_{𝑜} \in V$
81		opex	$⊢ ⟨1^{st} (s), 1^{st} (r)⟩ \in V$
82	80 81	opth	$⊢ ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩ = ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ \leftrightarrow (1_{𝑜} = 2_{𝑜} \land ⟨1^{st} (s), 1^{st} (r)⟩ = ⟨i, 1^{st} (u)⟩)$
83		1one2o	$⊢ 1_{𝑜} \neq 2_{𝑜}$
84		df-ne	$⊢ 1_{𝑜} \neq 2_{𝑜} \leftrightarrow \neg 1_{𝑜} = 2_{𝑜}$
85		pm2.21	$⊢ \neg 1_{𝑜} = 2_{𝑜} \to (1_{𝑜} = 2_{𝑜} \to y = w)$
86	84 85	sylbi	$⊢ 1_{𝑜} \neq 2_{𝑜} \to (1_{𝑜} = 2_{𝑜} \to y = w)$
87	83 86	ax-mp	$⊢ 1_{𝑜} = 2_{𝑜} \to y = w$
88	87	adantr	$⊢ (1_{𝑜} = 2_{𝑜} \land ⟨1^{st} (s), 1^{st} (r)⟩ = ⟨i, 1^{st} (u)⟩) \to y = w$
89	82 88	sylbi	$⊢ ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩ = ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ \to y = w$
90	79 89	sylbi	$⊢ 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = [\forall_{𝑔} i 1^{st} (u)] \to y = w$
91	73 90	biimtrdi	$⊢ x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to y = w)$
92	91	adantr	$⊢ (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to y = w)$
93	92	com12	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w)$
94	93	adantr	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w)$
95	94	a1i	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
96	95	rexlimdva	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
97	72 96	jaod	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to ((\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
98	97	rexlimdva	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in 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 w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
99		simp-4l	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to Fun S (suc N)$
100	58	adantr	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to (s \in S (suc N) \land r \in S (suc N))$
101		ssel	$⊢ S (N) \subseteq S (suc N) \to (u \in S (N) \to u \in S (suc N))$
102	101	ad3antlr	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \to (u \in S (N) \to u \in S (suc N))$
103	102	com12	$⊢ u \in S (N) \to ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \to u \in S (suc N))$
104	103	adantr	$⊢ (u \in S (N) \land v \in (S (suc N) ∖ S (N))) \to ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \to u \in S (suc N))$
105	104	impcom	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to u \in S (suc N)$
106		eldifi	$⊢ v \in (S (suc N) ∖ S (N)) \to v \in S (suc N)$
107	106	ad2antll	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to v \in S (suc N)$
108	105 107	jca	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to (u \in S (suc N) \land v \in S (suc N))$
109	99 100 108	3jca	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to (Fun S (suc N) \land (s \in S (suc N) \land r \in S (suc N)) \land (u \in S (suc N) \land v \in S (suc N)))$
110	109 64 67 68	syl3an	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w$
111	110	3exp	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
112	111	com23	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
113	112	rexlimdvva	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in 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 w = A) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
114	98 113	jaod	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in 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 w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = w))$
115	114	com23	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land r \in S (suc N)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
116	115	rexlimdva	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \to (\exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
117		eqeq1	$⊢ x = [\forall_{𝑔} j 1^{st} (s)] \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow [\forall_{𝑔} j 1^{st} (s)] = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
118		df-goal	$⊢ [\forall_{𝑔} j 1^{st} (s)] = ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩$
119		fvex	$⊢ 1^{st} (u) \in V$
120		fvex	$⊢ 1^{st} (v) \in V$
121		gonafv	$⊢ (1^{st} (u) \in V \land 1^{st} (v) \in V) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
122	119 120 121	mp2an	$⊢ 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
123	118 122	eqeq12i	$⊢ [\forall_{𝑔} j 1^{st} (s)] = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
124		2oex	$⊢ 2_{𝑜} \in V$
125		opex	$⊢ ⟨j, 1^{st} (s)⟩ \in V$
126	124 125	opth	$⊢ ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \leftrightarrow (2_{𝑜} = 1_{𝑜} \land ⟨j, 1^{st} (s)⟩ = ⟨1^{st} (u), 1^{st} (v)⟩)$
127	87	eqcoms	$⊢ 2_{𝑜} = 1_{𝑜} \to y = w$
128	127	adantr	$⊢ (2_{𝑜} = 1_{𝑜} \land ⟨j, 1^{st} (s)⟩ = ⟨1^{st} (u), 1^{st} (v)⟩) \to y = w$
129	126 128	sylbi	$⊢ ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \to y = w$
130	123 129	sylbi	$⊢ [\forall_{𝑔} j 1^{st} (s)] = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to y = w$
131	117 130	biimtrdi	$⊢ x = [\forall_{𝑔} j 1^{st} (s)] \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to y = w)$
132	131	adantr	$⊢ (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to y = w)$
133	132	com12	$⊢ x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w)$
134	133	adantr	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w)$
135	134	rexlimivw	$⊢ \exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w)$
136	135	a1i	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \to (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
137		eqeq1	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to (x = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)])$
138	78 118	eqeq12i	$⊢ [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩$
139		opex	$⊢ ⟨i, 1^{st} (u)⟩ \in V$
140	124 139	opth	$⊢ ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ \leftrightarrow (2_{𝑜} = 2_{𝑜} \land ⟨i, 1^{st} (u)⟩ = ⟨j, 1^{st} (s)⟩)$
141		vex	$⊢ i \in V$
142	141 119	opth	$⊢ ⟨i, 1^{st} (u)⟩ = ⟨j, 1^{st} (s)⟩ \leftrightarrow (i = j \land 1^{st} (u) = 1^{st} (s))$
143	142	anbi2i	$⊢ (2_{𝑜} = 2_{𝑜} \land ⟨i, 1^{st} (u)⟩ = ⟨j, 1^{st} (s)⟩) \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s)))$
144	138 140 143	3bitri	$⊢ [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s)))$
145	137 144	bitrdi	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to (x = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))))$
146	145	adantl	$⊢ ((((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to (x = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))))$
147	56	a1i	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (s \in (S (suc N) ∖ S (N)) \to s \in S (suc N))$
148		funfv1st2nd	$⊢ (Fun S (suc N) \land s \in S (suc N)) \to S (suc N) (1^{st} (s)) = 2^{nd} (s)$
149	148	ex	$⊢ Fun S (suc N) \to (s \in S (suc N) \to S (suc N) (1^{st} (s)) = 2^{nd} (s))$
150	149	adantr	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (s \in S (suc N) \to S (suc N) (1^{st} (s)) = 2^{nd} (s))$
151		funfv1st2nd	$⊢ (Fun S (suc N) \land u \in S (suc N)) \to S (suc N) (1^{st} (u)) = 2^{nd} (u)$
152	151	ex	$⊢ Fun S (suc N) \to (u \in S (suc N) \to S (suc N) (1^{st} (u)) = 2^{nd} (u))$
153	152	adantr	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (u \in S (suc N) \to S (suc N) (1^{st} (u)) = 2^{nd} (u))$
154		fveqeq2	$⊢ 1^{st} (u) = 1^{st} (s) \to (S (suc N) (1^{st} (u)) = 2^{nd} (u) \leftrightarrow S (suc N) (1^{st} (s)) = 2^{nd} (u))$
155		eqtr2	$⊢ (S (suc N) (1^{st} (s)) = 2^{nd} (u) \land S (suc N) (1^{st} (s)) = 2^{nd} (s)) \to 2^{nd} (u) = 2^{nd} (s)$
156	29	eqcomd	$⊢ i = j \to \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) = \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})})$
157	156	adantl	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) = \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})})$
158		simpl	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to 2^{nd} (u) = 2^{nd} (s)$
159	158	eqcomd	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to 2^{nd} (s) = 2^{nd} (u)$
160	157 159	eleq12d	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to (\{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s) \leftrightarrow \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u))$
161	160	ralbidv	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to (\forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s) \leftrightarrow \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u))$
162	161	rabbidv	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
163	162 3	eqtr4di	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} = B$
164		eqeq12	$⊢ (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \land w = B) \to (y = w \leftrightarrow \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} = B)$
165	163 164	syl5ibrcom	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to ((y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \land w = B) \to y = w)$
166	165	exp4b	$⊢ 2^{nd} (u) = 2^{nd} (s) \to (i = j \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))$
167	155 166	syl	$⊢ (S (suc N) (1^{st} (s)) = 2^{nd} (u) \land S (suc N) (1^{st} (s)) = 2^{nd} (s)) \to (i = j \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))$
168	167	ex	$⊢ S (suc N) (1^{st} (s)) = 2^{nd} (u) \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to (i = j \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w))))$
169	154 168	biimtrdi	$⊢ 1^{st} (u) = 1^{st} (s) \to (S (suc N) (1^{st} (u)) = 2^{nd} (u) \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to (i = j \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))))$
170	169	com24	$⊢ 1^{st} (u) = 1^{st} (s) \to (i = j \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to (S (suc N) (1^{st} (u)) = 2^{nd} (u) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))))$
171	170	impcom	$⊢ (i = j \land 1^{st} (u) = 1^{st} (s)) \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to (S (suc N) (1^{st} (u)) = 2^{nd} (u) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w))))$
172	171	com13	$⊢ S (suc N) (1^{st} (u)) = 2^{nd} (u) \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w))))$
173	60 153 172	syl56	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (u \in (S (suc N) ∖ S (N)) \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))))$
174	173	com23	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (S (suc N) (1^{st} (s)) = 2^{nd} (s) \to (u \in (S (suc N) ∖ S (N)) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))))$
175	147 150 174	3syld	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (s \in (S (suc N) ∖ S (N)) \to (u \in (S (suc N) ∖ S (N)) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))))$
176	175	imp	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \to (u \in (S (suc N) ∖ S (N)) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w))))$
177	176	adantr	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \to (u \in (S (suc N) ∖ S (N)) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w))))$
178	177	imp	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))$
179	178	adantld	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \to ((2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))$
180	179	ad2antrr	$⊢ ((((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to ((2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))$
181	146 180	sylbid	$⊢ ((((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to (x = [\forall_{𝑔} j 1^{st} (s)] \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (w = B \to y = w)))$
182	181	impd	$⊢ ((((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (w = B \to y = w))$
183	182	ex	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (w = B \to y = w)))$
184	183	com34	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to (w = B \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w)))$
185	184	impd	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
186	185	rexlimdva	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
187	136 186	jaod	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in (S (suc N) ∖ S (N))) \to ((\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
188	187	rexlimdva	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
189	134	a1i	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in S (N)) \land v \in (S (suc N) ∖ S (N))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
190	189	rexlimdva	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \land u \in S (N)) \to (\exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
191	190	rexlimdva	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
192	188 191	jaod	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = w))$
193	192	com23	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \land j \in ω) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
194	193	rexlimdva	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \to (\exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
195	116 194	jaod	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land s \in (S (suc N) ∖ S (N))) \to ((\exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
196	195	rexlimdva	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (\exists s \in (S (suc N) ∖ S (N)) (\exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
197		simplll	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \to Fun S (suc N)$
198		ssel	$⊢ S (N) \subseteq S (suc N) \to (s \in S (N) \to s \in S (suc N))$
199	198	adantrd	$⊢ S (N) \subseteq S (suc N) \to ((s \in S (N) \land r \in (S (suc N) ∖ S (N))) \to s \in S (suc N))$
200	199	adantl	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to ((s \in S (N) \land r \in (S (suc N) ∖ S (N))) \to s \in S (suc N))$
201	200	imp	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to s \in S (suc N)$
202		eldifi	$⊢ r \in (S (suc N) ∖ S (N)) \to r \in S (suc N)$
203	202	ad2antll	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to r \in S (suc N)$
204	201 203	jca	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to (s \in S (suc N) \land r \in S (suc N))$
205	204	adantr	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \to (s \in S (suc N) \land r \in S (suc N))$
206	60	anim1i	$⊢ (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N)) \to (u \in S (suc N) \land v \in S (suc N))$
207	206	adantl	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \to (u \in S (suc N) \land v \in S (suc N))$
208	197 205 207	3jca	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \to (Fun S (suc N) \land (s \in S (suc N) \land r \in S (suc N)) \land (u \in S (suc N) \land v \in S (suc N)))$
209	208	adantr	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \land ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to (Fun S (suc N) \land (s \in S (suc N) \land r \in S (suc N)) \land (u \in S (suc N) \land v \in S (suc N)))$
210		simprl	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \land ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
211	67	ad2antll	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \land ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
212	209 210 211 68	syl3anc	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \land ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to y = w$
213	212	exp32	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in (S (suc N) ∖ S (N)) \land v \in S (suc N))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
214	213	impancom	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to ((u \in (S (suc N) ∖ S (N)) \land v \in S (suc N)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
215	214	expdimp	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \land u \in (S (suc N) ∖ S (N))) \to (v \in S (suc N) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
216	215	rexlimdv	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \land u \in (S (suc N) ∖ S (N))) \to (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w)$
217	91	adantrd	$⊢ x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to y = w)$
218	217	adantr	$⊢ (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to y = w)$
219	218	ad3antlr	$⊢ (((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \land u \in (S (suc N) ∖ S (N))) \land i \in ω) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to y = w)$
220	219	rexlimdva	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \land u \in (S (suc N) ∖ S (N))) \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B) \to y = w)$
221	216 220	jaod	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \land u \in (S (suc N) ∖ S (N))) \to ((\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \to y = w)$
222	221	rexlimdva	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \to y = w)$
223		simplll	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to Fun S (suc N)$
224	204	adantr	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to (s \in S (suc N) \land r \in S (suc N))$
225	101	adantl	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (u \in S (N) \to u \in S (suc N))$
226	225	adantr	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to (u \in S (N) \to u \in S (suc N))$
227	226	com12	$⊢ u \in S (N) \to (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to u \in S (suc N))$
228	227	adantr	$⊢ (u \in S (N) \land v \in (S (suc N) ∖ S (N))) \to (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to u \in S (suc N))$
229	228	impcom	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to u \in S (suc N)$
230	106	ad2antll	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to v \in S (suc N)$
231	229 230	jca	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to (u \in S (suc N) \land v \in S (suc N))$
232	223 224 231	3jca	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to (Fun S (suc N) \land (s \in S (suc N) \land r \in S (suc N)) \land (u \in S (suc N) \land v \in S (suc N)))$
233	232 64 67 68	syl3an	$⊢ ((((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w$
234	233	3exp	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (u \in S (N) \land v \in (S (suc N) ∖ S (N)))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
235	234	impancom	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to ((u \in S (N) \land v \in (S (suc N) ∖ S (N))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w))$
236	235	rexlimdvv	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \to y = w)$
237	222 236	jaod	$⊢ (((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w)$
238	237	ex	$⊢ ((Fun S (suc N) \land S (N) \subseteq S (suc N)) \land (s \in S (N) \land r \in (S (suc N) ∖ S (N)))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
239	238	rexlimdvva	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to (\exists s \in S (N) \exists r \in (S (suc N) ∖ S (N)) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
240	196 239	jaod	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to ((\exists s \in (S (suc N) ∖ S (N)) (\exists r \in S (suc N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨j, z⟩\} \cup ({a ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})) \lor \exists s \in S (N) \exists r \in (S (suc N) ∖ S (N)) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
241	54 240	biimtrid	$⊢ (Fun S (suc N) \land 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)) \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) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)) \to y = w))$
242	241	impd	$⊢ (Fun S (suc N) \land 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)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A)) \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to y = w)$
243	242	alrimivv	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to \forall y \forall w (((\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)) \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to y = w)$
244		eqeq1	$⊢ y = w \to (y = A \leftrightarrow w = A)$
245	244	anbi2d	$⊢ y = w \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))$
246	245	rexbidv	$⊢ y = w \to (\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 w = A))$
247		eqeq1	$⊢ y = w \to (y = B \leftrightarrow w = B)$
248	247	anbi2d	$⊢ y = w \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = B) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B))$
249	248	rexbidv	$⊢ y = w \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B) \leftrightarrow \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B))$
250	246 249	orbi12d	$⊢ y = w \to ((\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 w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)))$
251	250	rexbidv	$⊢ y = w \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)) \leftrightarrow \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)))$
252	245	2rexbidv	$⊢ y = w \to (\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 (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))$
253	251 252	orbi12d	$⊢ y = w \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)) \leftrightarrow (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A)))$
254	253	mo4	$⊢ \exists^{*} 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 \forall y \forall w (((\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)) \land (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = A))) \to y = w)$
255	243 254	sylibr	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to \exists^{*} 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))$
256	255	alrimiv	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to \forall x \exists^{*} 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))$
257		funopab	$⊢ Fun \{⟨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 \forall x \exists^{*} 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))$
258	256 257	sylibr	$⊢ (Fun S (suc N) \land S (N) \subseteq S (suc N)) \to Fun \{⟨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 satffunlem2lem1

Proof