satfv1

Description: The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023)

		Ref	Expression
	Hypothesis	satfv1.s	$⊢ S = M Sat E$
	Assertion	satfv1	$⊢ (M \in V \land E \in W) \to S (1_{𝑜}) = S (\emptyset) \cup \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))\}$

Proof

Step	Hyp	Ref	Expression
1		satfv1.s	$⊢ S = M Sat E$
2		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
3	2	fveq2i	$⊢ S (1_{𝑜}) = S (suc \emptyset)$
4	3	a1i	$⊢ (M \in V \land E \in W) \to S (1_{𝑜}) = S (suc \emptyset)$
5		peano1	$⊢ \emptyset \in ω$
6	1	satfvsuc	$⊢ (M \in V \land E \in W \land \emptyset \in ω) \to S (suc \emptyset) = S (\emptyset) \cup \{⟨x, y⟩ \| \exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\}))\}$
7	5 6	mp3an3	$⊢ (M \in V \land E \in W) \to S (suc \emptyset) = S (\emptyset) \cup \{⟨x, y⟩ \| \exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\}))\}$
8	1	satfv0	$⊢ (M \in V \land E \in W) \to S (\emptyset) = \{⟨e, b⟩ \| \exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
9	8	rexeqdv	$⊢ (M \in V \land E \in W) \to (\exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\})) \leftrightarrow \exists o \in \{⟨e, b⟩ \| \exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})\} (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\})))$
10		eqid	$⊢ \{⟨e, b⟩ \| \exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})\} = \{⟨e, b⟩ \| \exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
11		vex	$⊢ e \in V$
12		vex	$⊢ b \in V$
13	11 12	op1std	$⊢ o = ⟨e, b⟩ \to 1^{st} (o) = e$
14	13	oveq1d	$⊢ o = ⟨e, b⟩ \to 1^{st} (o) ⊼_{𝑔} 1^{st} (p) = e ⊼_{𝑔} 1^{st} (p)$
15	14	eqeq2d	$⊢ o = ⟨e, b⟩ \to (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \leftrightarrow x = e ⊼_{𝑔} 1^{st} (p))$
16	11 12	op2ndd	$⊢ o = ⟨e, b⟩ \to 2^{nd} (o) = b$
17	16	ineq1d	$⊢ o = ⟨e, b⟩ \to 2^{nd} (o) \cap 2^{nd} (p) = b \cap 2^{nd} (p)$
18	17	difeq2d	$⊢ o = ⟨e, b⟩ \to (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p)) = (M^{ω}) ∖ (b \cap 2^{nd} (p))$
19	18	eqeq2d	$⊢ o = ⟨e, b⟩ \to (y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p)) \leftrightarrow y = (M^{ω}) ∖ (b \cap 2^{nd} (p)))$
20	15 19	anbi12d	$⊢ o = ⟨e, b⟩ \to ((x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \leftrightarrow (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))))$
21	20	rexbidv	$⊢ o = ⟨e, b⟩ \to (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \leftrightarrow \exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))))$
22		eqidd	$⊢ o = ⟨e, b⟩ \to n = n$
23	22 13	goaleq12d	$⊢ o = ⟨e, b⟩ \to [\forall_{𝑔} n 1^{st} (o)] = [\forall_{𝑔} n e]$
24	23	eqeq2d	$⊢ o = ⟨e, b⟩ \to (x = [\forall_{𝑔} n 1^{st} (o)] \leftrightarrow x = [\forall_{𝑔} n e])$
25	16	eleq2d	$⊢ o = ⟨e, b⟩ \to (\{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o) \leftrightarrow \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b)$
26	25	ralbidv	$⊢ o = ⟨e, b⟩ \to (\forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o) \leftrightarrow \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b)$
27	26	rabbidv	$⊢ o = ⟨e, b⟩ \to \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}$
28	27	eqeq2d	$⊢ o = ⟨e, b⟩ \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\} \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})$
29	24 28	anbi12d	$⊢ o = ⟨e, b⟩ \to ((x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\}) \leftrightarrow (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))$
30	29	rexbidv	$⊢ o = ⟨e, b⟩ \to (\exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\}) \leftrightarrow \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))$
31	21 30	orbi12d	$⊢ o = ⟨e, b⟩ \to ((\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\})) \leftrightarrow (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
32	10 31	rexopabb	$⊢ \exists o \in \{⟨e, b⟩ \| \exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})\} (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\})) \leftrightarrow \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
33	9 32	syl6bb	$⊢ (M \in V \land E \in W) \to (\exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\})) \leftrightarrow \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))))$
34	1	satfv0	$⊢ (M \in V \land E \in W) \to S (\emptyset) = \{⟨c, d⟩ \| \exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\})\}$
35	34	rexeqdv	$⊢ (M \in V \land E \in W) \to (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \leftrightarrow \exists p \in \{⟨c, d⟩ \| \exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\})\} (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))))$
36		eqid	$⊢ \{⟨c, d⟩ \| \exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\})\} = \{⟨c, d⟩ \| \exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\})\}$
37		vex	$⊢ c \in V$
38		vex	$⊢ d \in V$
39	37 38	op1std	$⊢ p = ⟨c, d⟩ \to 1^{st} (p) = c$
40	39	oveq2d	$⊢ p = ⟨c, d⟩ \to e ⊼_{𝑔} 1^{st} (p) = e ⊼_{𝑔} c$
41	40	eqeq2d	$⊢ p = ⟨c, d⟩ \to (x = e ⊼_{𝑔} 1^{st} (p) \leftrightarrow x = e ⊼_{𝑔} c)$
42	37 38	op2ndd	$⊢ p = ⟨c, d⟩ \to 2^{nd} (p) = d$
43	42	ineq2d	$⊢ p = ⟨c, d⟩ \to b \cap 2^{nd} (p) = b \cap d$
44	43	difeq2d	$⊢ p = ⟨c, d⟩ \to (M^{ω}) ∖ (b \cap 2^{nd} (p)) = (M^{ω}) ∖ (b \cap d)$
45	44	eqeq2d	$⊢ p = ⟨c, d⟩ \to (y = (M^{ω}) ∖ (b \cap 2^{nd} (p)) \leftrightarrow y = (M^{ω}) ∖ (b \cap d))$
46	41 45	anbi12d	$⊢ p = ⟨c, d⟩ \to ((x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \leftrightarrow (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d)))$
47	36 46	rexopabb	$⊢ \exists p \in \{⟨c, d⟩ \| \exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\})\} (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \leftrightarrow \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d)))$
48	35 47	syl6bb	$⊢ (M \in V \land E \in W) \to (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \leftrightarrow \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))))$
49	48	orbi1d	$⊢ (M \in V \land E \in W) \to ((\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})) \leftrightarrow (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
50	49	anbi2d	$⊢ (M \in V \land E \in W) \to ((\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))))$
51	50	2exbidv	$⊢ (M \in V \land E \in W) \to (\exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))))$
52		r19.41vv	$⊢ \exists i \in ω \exists j \in ω ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
53		oveq1	$⊢ e = i \in_{𝑔} j \to e ⊼_{𝑔} c = (i \in_{𝑔} j) ⊼_{𝑔} c$
54	53	eqeq2d	$⊢ e = i \in_{𝑔} j \to (x = e ⊼_{𝑔} c \leftrightarrow x = (i \in_{𝑔} j) ⊼_{𝑔} c)$
55		ineq1	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to b \cap d = \{a \in (M^{ω}) \| a (i) E a (j)\} \cap d$
56	55	difeq2d	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to (M^{ω}) ∖ (b \cap d) = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)$
57	56	eqeq2d	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to (y = (M^{ω}) ∖ (b \cap d) \leftrightarrow y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))$
58	54 57	bi2anan9	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d)) \leftrightarrow (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
59	58	anbi2d	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \leftrightarrow (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))))$
60	59	2exbidv	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \leftrightarrow \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))))$
61		eqidd	$⊢ e = i \in_{𝑔} j \to n = n$
62		id	$⊢ e = i \in_{𝑔} j \to e = i \in_{𝑔} j$
63	61 62	goaleq12d	$⊢ e = i \in_{𝑔} j \to [\forall_{𝑔} n e] = [\forall_{𝑔} n (i \in_{𝑔} j)]$
64	63	eqeq2d	$⊢ e = i \in_{𝑔} j \to (x = [\forall_{𝑔} n e] \leftrightarrow x = [\forall_{𝑔} n (i \in_{𝑔} j)])$
65		nfrab1	$⊢ \underline{Ⅎ} a \{a \in (M^{ω}) \| a (i) E a (j)\}$
66	65	nfeq2	$⊢ Ⅎ a b = \{a \in (M^{ω}) \| a (i) E a (j)\}$
67		eleq2	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to (\{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b \leftrightarrow \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\})$
68	67	ralbidv	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to (\forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b \leftrightarrow \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\})$
69	66 68	rabbid	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}$
70	69	eqeq2d	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\} \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})$
71	64 70	bi2anan9	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}) \leftrightarrow (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))$
72	71	rexbidv	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to (\exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}) \leftrightarrow \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))$
73	60 72	orbi12d	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})) \leftrightarrow (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})))$
74	73	adantl	$⊢ ((i \in ω \land j \in ω) \land (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to ((\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})) \leftrightarrow (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})))$
75		r19.41vv	$⊢ \exists k \in ω \exists l \in ω ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \leftrightarrow (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
76		oveq2	$⊢ c = k \in_{𝑔} l \to (i \in_{𝑔} j) ⊼_{𝑔} c = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l)$
77	76	adantr	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to (i \in_{𝑔} j) ⊼_{𝑔} c = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l)$
78	77	eqeq2d	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to (x = (i \in_{𝑔} j) ⊼_{𝑔} c \leftrightarrow x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
79		ineq2	$⊢ d = \{a \in (M^{ω}) \| a (k) E a (l)\} \to \{a \in (M^{ω}) \| a (i) E a (j)\} \cap d = \{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}$
80	79	difeq2d	$⊢ d = \{a \in (M^{ω}) \| a (k) E a (l)\} \to (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d) = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\})$
81		inrab	$⊢ \{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| (a (i) E a (j) \land a (k) E a (l))\}$
82	81	difeq2i	$⊢ (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}) = (M^{ω}) ∖ \{a \in (M^{ω}) \| (a (i) E a (j) \land a (k) E a (l))\}$
83		notrab	$⊢ (M^{ω}) ∖ \{a \in (M^{ω}) \| (a (i) E a (j) \land a (k) E a (l))\} = \{a \in (M^{ω}) \| \neg (a (i) E a (j) \land a (k) E a (l))\}$
84		ianor	$⊢ \neg (a (i) E a (j) \land a (k) E a (l)) \leftrightarrow (\neg a (i) E a (j) \lor \neg a (k) E a (l))$
85	84	rabbii	$⊢ \{a \in (M^{ω}) \| \neg (a (i) E a (j) \land a (k) E a (l))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}$
86	82 83 85	3eqtri	$⊢ (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}) = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}$
87	80 86	syl6eq	$⊢ d = \{a \in (M^{ω}) \| a (k) E a (l)\} \to (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d) = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}$
88	87	eqeq2d	$⊢ d = \{a \in (M^{ω}) \| a (k) E a (l)\} \to (y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d) \leftrightarrow y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
89	88	adantl	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to (y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d) \leftrightarrow y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
90	78 89	anbi12d	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to ((x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)) \leftrightarrow (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}))$
91	90	biimpa	$⊢ ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \to (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
92	91	reximi	$⊢ \exists l \in ω ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \to \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
93	92	reximi	$⊢ \exists k \in ω \exists l \in ω ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \to \exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
94	75 93	sylbir	$⊢ (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \to \exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
95	94	exlimivv	$⊢ \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \to \exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
96	95	a1i	$⊢ ((i \in ω \land j \in ω) \land (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \to \exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}))$
97		simpr	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to n \in ω$
98		simpll	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to i \in ω$
99		simplr	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to j \in ω$
100		fveq1	$⊢ a = b \to a (i) = b (i)$
101		fveq1	$⊢ a = b \to a (j) = b (j)$
102	100 101	breq12d	$⊢ a = b \to (a (i) E a (j) \leftrightarrow b (i) E b (j))$
103	102	cbvrabv	$⊢ \{a \in (M^{ω}) \| a (i) E a (j)\} = \{b \in (M^{ω}) \| b (i) E b (j)\}$
104	103	eleq2i	$⊢ \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\} \leftrightarrow \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{b \in (M^{ω}) \| b (i) E b (j)\}$
105	104	ralbii	$⊢ \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\} \leftrightarrow \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{b \in (M^{ω}) \| b (i) E b (j)\}$
106	105	rabbii	$⊢ \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{b \in (M^{ω}) \| b (i) E b (j)\}\}$
107		satfv1lem	$⊢ (n \in ω \land i \in ω \land j \in ω) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{b \in (M^{ω}) \| b (i) E b (j)\}\} = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}$
108	106 107	syl5eq	$⊢ (n \in ω \land i \in ω \land j \in ω) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\} = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}$
109	97 98 99 108	syl3anc	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\} = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}$
110	109	eqeq2d	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\} \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})$
111	110	biimpd	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\} \to y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})$
112	111	anim2d	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to ((x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}) \to (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
113	112	reximdva	$⊢ (i \in ω \land j \in ω) \to (\exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}) \to \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
114	113	adantr	$⊢ ((i \in ω \land j \in ω) \land (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to (\exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}) \to \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
115	96 114	orim12d	$⊢ ((i \in ω \land j \in ω) \land (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to ((\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})) \to (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})))$
116	74 115	sylbid	$⊢ ((i \in ω \land j \in ω) \land (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to ((\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})) \to (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})))$
117	116	expimpd	$⊢ (i \in ω \land j \in ω) \to (((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \to (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})))$
118	117	reximdva	$⊢ i \in ω \to (\exists j \in ω ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \to \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})))$
119	118	reximia	$⊢ \exists i \in ω \exists j \in ω ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \to \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
120	52 119	sylbir	$⊢ (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \to \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
121	120	exlimivv	$⊢ \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \to \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
122		ovex	$⊢ i \in_{𝑔} j \in V$
123		ovex	$⊢ M^{ω} \in V$
124	123	rabex	$⊢ \{a \in (M^{ω}) \| a (i) E a (j)\} \in V$
125	122 124	pm3.2i	$⊢ (i \in_{𝑔} j \in V \land \{a \in (M^{ω}) \| a (i) E a (j)\} \in V)$
126		eqid	$⊢ k \in_{𝑔} l = k \in_{𝑔} l$
127		eqid	$⊢ \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| a (k) E a (l)\}$
128	126 127	pm3.2i	$⊢ (k \in_{𝑔} l = k \in_{𝑔} l \land \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| a (k) E a (l)\})$
129	86	eqcomi	$⊢ \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\} = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\})$
130	129	eqeq2i	$⊢ y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\} \leftrightarrow y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\})$
131	130	biimpi	$⊢ y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\} \to y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\})$
132	131	anim2i	$⊢ (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \to (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}))$
133		ovex	$⊢ k \in_{𝑔} l \in V$
134	123	rabex	$⊢ \{a \in (M^{ω}) \| a (k) E a (l)\} \in V$
135		eqeq1	$⊢ c = k \in_{𝑔} l \to (c = k \in_{𝑔} l \leftrightarrow k \in_{𝑔} l = k \in_{𝑔} l)$
136		eqeq1	$⊢ d = \{a \in (M^{ω}) \| a (k) E a (l)\} \to (d = \{a \in (M^{ω}) \| a (k) E a (l)\} \leftrightarrow \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| a (k) E a (l)\})$
137	135 136	bi2anan9	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \leftrightarrow (k \in_{𝑔} l = k \in_{𝑔} l \land \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| a (k) E a (l)\}))$
138	76	eqeq2d	$⊢ c = k \in_{𝑔} l \to (x = (i \in_{𝑔} j) ⊼_{𝑔} c \leftrightarrow x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
139	80	eqeq2d	$⊢ d = \{a \in (M^{ω}) \| a (k) E a (l)\} \to (y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d) \leftrightarrow y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}))$
140	138 139	bi2anan9	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to ((x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)) \leftrightarrow (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\})))$
141	137 140	anbi12d	$⊢ (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \to (((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \leftrightarrow ((k \in_{𝑔} l = k \in_{𝑔} l \land \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}))))$
142	133 134 141	spc2ev	$⊢ ((k \in_{𝑔} l = k \in_{𝑔} l \land \{a \in (M^{ω}) \| a (k) E a (l)\} = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap \{a \in (M^{ω}) \| a (k) E a (l)\}))) \to \exists c \exists d ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
143	128 132 142	sylancr	$⊢ (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \to \exists c \exists d ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
144	143	reximi	$⊢ \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \to \exists l \in ω \exists c \exists d ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
145	144	reximi	$⊢ \exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \to \exists k \in ω \exists l \in ω \exists c \exists d ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
146	75	bicomi	$⊢ (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \leftrightarrow \exists k \in ω \exists l \in ω ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
147	146	2exbii	$⊢ \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \leftrightarrow \exists c \exists d \exists k \in ω \exists l \in ω ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
148		2ex2rexrot	$⊢ \exists c \exists d \exists k \in ω \exists l \in ω ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \leftrightarrow \exists k \in ω \exists l \in ω \exists c \exists d ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
149	147 148	bitri	$⊢ \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \leftrightarrow \exists k \in ω \exists l \in ω \exists c \exists d ((c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
150	145 149	sylibr	$⊢ \exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \to \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d)))$
151	150	a1i	$⊢ (i \in ω \land j \in ω) \to (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \to \exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))))$
152	109	eqcomd	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}$
153	152	eqeq2d	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to (y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\} \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})$
154	153	biimpd	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to (y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\} \to y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})$
155	154	anim2d	$⊢ ((i \in ω \land j \in ω) \land n \in ω) \to ((x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}) \to (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))$
156	155	reximdva	$⊢ (i \in ω \land j \in ω) \to (\exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}) \to \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))$
157	151 156	orim12d	$⊢ (i \in ω \land j \in ω) \to ((\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})) \to (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})))$
158	157	imp	$⊢ ((i \in ω \land j \in ω) \land (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))) \to (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))$
159		eqid	$⊢ i \in_{𝑔} j = i \in_{𝑔} j$
160		eqid	$⊢ \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}$
161	159 160	pm3.2i	$⊢ (i \in_{𝑔} j = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
162	158 161	jctil	$⊢ ((i \in ω \land j \in ω) \land (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))) \to ((i \in_{𝑔} j = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\})))$
163		eqeq1	$⊢ e = i \in_{𝑔} j \to (e = i \in_{𝑔} j \leftrightarrow i \in_{𝑔} j = i \in_{𝑔} j)$
164		eqeq1	$⊢ b = \{a \in (M^{ω}) \| a (i) E a (j)\} \to (b = \{a \in (M^{ω}) \| a (i) E a (j)\} \leftrightarrow \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
165	163 164	bi2anan9	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow (i \in_{𝑔} j = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
166	165 73	anbi12d	$⊢ (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to (((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow ((i \in_{𝑔} j = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))))$
167	166	spc2egv	$⊢ (i \in_{𝑔} j \in V \land \{a \in (M^{ω}) \| a (i) E a (j)\} \in V) \to (((i \in_{𝑔} j = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = (i \in_{𝑔} j) ⊼_{𝑔} c \land y = (M^{ω}) ∖ (\{a \in (M^{ω}) \| a (i) E a (j)\} \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in \{a \in (M^{ω}) \| a (i) E a (j)\}\}))) \to \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))))$
168	125 162 167	mpsyl	$⊢ ((i \in ω \land j \in ω) \land (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))) \to \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
169	168	ex	$⊢ (i \in ω \land j \in ω) \to ((\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})) \to \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))))$
170	169	reximdva	$⊢ i \in ω \to (\exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})) \to \exists j \in ω \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))))$
171	170	reximia	$⊢ \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})) \to \exists i \in ω \exists j \in ω \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
172	52	bicomi	$⊢ (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists i \in ω \exists j \in ω ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
173	172	2exbii	$⊢ \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists e \exists b \exists i \in ω \exists j \in ω ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
174		2ex2rexrot	$⊢ \exists e \exists b \exists i \in ω \exists j \in ω ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists i \in ω \exists j \in ω \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
175	173 174	bitri	$⊢ \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists i \in ω \exists j \in ω \exists e \exists b ((e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
176	171 175	sylibr	$⊢ \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})) \to \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\})))$
177	121 176	impbii	$⊢ \exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists c \exists d (\exists k \in ω \exists l \in ω (c = k \in_{𝑔} l \land d = \{a \in (M^{ω}) \| a (k) E a (l)\}) \land (x = e ⊼_{𝑔} c \land y = (M^{ω}) ∖ (b \cap d))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))$
178	51 177	syl6bb	$⊢ (M \in V \land E \in W) \to (\exists e \exists b (\exists i \in ω \exists j \in ω (e = i \in_{𝑔} j \land b = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land (\exists p \in S (\emptyset) (x = e ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (b \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n e] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in b\}))) \leftrightarrow \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})))$
179	33 178	bitrd	$⊢ (M \in V \land E \in W) \to (\exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\})) \leftrightarrow \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\})))$
180	179	opabbidv	$⊢ (M \in V \land E \in W) \to \{⟨x, y⟩ \| \exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\}))\} = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))\}$
181	180	uneq2d	$⊢ (M \in V \land E \in W) \to S (\emptyset) \cup \{⟨x, y⟩ \| \exists o \in S (\emptyset) (\exists p \in S (\emptyset) (x = 1^{st} (o) ⊼_{𝑔} 1^{st} (p) \land y = (M^{ω}) ∖ (2^{nd} (o) \cap 2^{nd} (p))) \lor \exists n \in ω (x = [\forall_{𝑔} n 1^{st} (o)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨n, z⟩\} \cup ({a ↾}_{(ω ∖ \{n\})}) \in 2^{nd} (o)\}))\} = S (\emptyset) \cup \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))\}$
182	4 7 181	3eqtrd	$⊢ (M \in V \land E \in W) \to S (1_{𝑜}) = S (\emptyset) \cup \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \lor \exists n \in ω (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \land y = \{a \in (M^{ω}) \| \forall z \in M if- (i = n, if- (j = n, z E z, z E a (j)), if- (j = n, a (i) E z, a (i) E a (j)))\}))\}$

Metamath Proof Explorer

Theorem satfv1

Proof