satfv1fvfmla1

Description: The value of the satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023)

		Ref	Expression
	Hypothesis	satfv1fvfmla1.x	$⊢ X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
	Assertion	satfv1fvfmla1	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat E) (1_{𝑜}) (X) = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}$

Proof

Step	Hyp	Ref	Expression
1		satfv1fvfmla1.x	$⊢ X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
2		simpl	$⊢ (M \in V \land E \in W) \to M \in V$
3		simpr	$⊢ (M \in V \land E \in W) \to E \in W$
4		1onn	$⊢ 1_{𝑜} \in ω$
5	4	a1i	$⊢ (M \in V \land E \in W) \to 1_{𝑜} \in ω$
6	2 3 5	3jca	$⊢ (M \in V \land E \in W) \to (M \in V \land E \in W \land 1_{𝑜} \in ω)$
7	6	3ad2ant1	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M \in V \land E \in W \land 1_{𝑜} \in ω)$
8		satffun	$⊢ (M \in V \land E \in W \land 1_{𝑜} \in ω) \to Fun (M Sat E) (1_{𝑜})$
9	7 8	syl	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to Fun (M Sat E) (1_{𝑜})$
10		simp2l	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to I \in ω$
11		simp2r	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to J \in ω$
12		simp3l	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to K \in ω$
13		simp3r	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to L \in ω$
14		eqid	$⊢ \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}$
15	1 14	pm3.2i	$⊢ (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\})$
16	15	a1i	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\})$
17		oveq1	$⊢ k = K \to k \in_{𝑔} l = K \in_{𝑔} l$
18	17	oveq2d	$⊢ k = K \to (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} l)$
19	18	eqeq2d	$⊢ k = K \to (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} l))$
20		fveq2	$⊢ k = K \to a (k) = a (K)$
21	20	breq1d	$⊢ k = K \to (a (k) E a (l) \leftrightarrow a (K) E a (l))$
22	21	notbid	$⊢ k = K \to (\neg a (k) E a (l) \leftrightarrow \neg a (K) E a (l))$
23	22	orbi2d	$⊢ k = K \to ((\neg a (I) E a (J) \lor \neg a (k) E a (l)) \leftrightarrow (\neg a (I) E a (J) \lor \neg a (K) E a (l)))$
24	23	rabbidv	$⊢ k = K \to \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (l))\}$
25	24	eqeq2d	$⊢ k = K \to (\{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\} \leftrightarrow \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (l))\})$
26	19 25	anbi12d	$⊢ k = K \to ((X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\}) \leftrightarrow (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (l))\}))$
27		oveq2	$⊢ l = L \to K \in_{𝑔} l = K \in_{𝑔} L$
28	27	oveq2d	$⊢ l = L \to (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} l) = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
29	28	eqeq2d	$⊢ l = L \to (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} l) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L))$
30		fveq2	$⊢ l = L \to a (l) = a (L)$
31	30	breq2d	$⊢ l = L \to (a (K) E a (l) \leftrightarrow a (K) E a (L))$
32	31	notbid	$⊢ l = L \to (\neg a (K) E a (l) \leftrightarrow \neg a (K) E a (L))$
33	32	orbi2d	$⊢ l = L \to ((\neg a (I) E a (J) \lor \neg a (K) E a (l)) \leftrightarrow (\neg a (I) E a (J) \lor \neg a (K) E a (L)))$
34	33	rabbidv	$⊢ l = L \to \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (l))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}$
35	34	eqeq2d	$⊢ l = L \to (\{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (l))\} \leftrightarrow \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\})$
36	29 35	anbi12d	$⊢ l = L \to ((X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (l))\}) \leftrightarrow (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}))$
37	26 36	rspc2ev	$⊢ (K \in ω \land L \in ω \land (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\})) \to \exists k \in ω \exists l \in ω (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\})$
38	12 13 16 37	syl3anc	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to \exists k \in ω \exists l \in ω (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\})$
39	38	orcd	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (\exists k \in ω \exists l \in ω (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
40		oveq1	$⊢ i = I \to i \in_{𝑔} j = I \in_{𝑔} j$
41	40	oveq1d	$⊢ i = I \to (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l)$
42	41	eqeq2d	$⊢ i = I \to (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
43		fveq2	$⊢ i = I \to a (i) = a (I)$
44	43	breq1d	$⊢ i = I \to (a (i) E a (j) \leftrightarrow a (I) E a (j))$
45	44	notbid	$⊢ i = I \to (\neg a (i) E a (j) \leftrightarrow \neg a (I) E a (j))$
46	45	orbi1d	$⊢ i = I \to ((\neg a (i) E a (j) \lor \neg a (k) E a (l)) \leftrightarrow (\neg a (I) E a (j) \lor \neg a (k) E a (l)))$
47	46	rabbidv	$⊢ i = I \to \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\}$
48	47	eqeq2d	$⊢ i = I \to (\{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\} \leftrightarrow \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\})$
49	42 48	anbi12d	$⊢ i = I \to ((X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \leftrightarrow (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\}))$
50	49	2rexbidv	$⊢ i = I \to (\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \leftrightarrow \exists k \in ω \exists l \in ω (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\}))$
51		eqidd	$⊢ i = I \to n = n$
52	51 40	goaleq12d	$⊢ i = I \to [\forall_{𝑔} n (i \in_{𝑔} j)] = [\forall_{𝑔} n (I \in_{𝑔} j)]$
53	52	eqeq2d	$⊢ i = I \to (X = [\forall_{𝑔} n (i \in_{𝑔} j)] \leftrightarrow X = [\forall_{𝑔} n (I \in_{𝑔} j)])$
54		eqeq1	$⊢ i = I \to (i = n \leftrightarrow I = n)$
55		biidd	$⊢ i = I \to (if- (j = n, z E z, z E a (j)) \leftrightarrow if- (j = n, z E z, z E a (j)))$
56	43	breq1d	$⊢ i = I \to (a (i) E z \leftrightarrow a (I) E z)$
57	56 44	ifpbi23d	$⊢ i = I \to (if- (j = n, a (i) E z, a (i) E a (j)) \leftrightarrow if- (j = n, a (I) E z, a (I) E a (j)))$
58	54 55 57	ifpbi123d	$⊢ i = I \to (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 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))))$
59	58	ralbidv	$⊢ i = I \to (\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 \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))))$
60	59	rabbidv	$⊢ i = I \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 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)))\}$
61	60	eqeq2d	$⊢ i = I \to (\{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\})$
62	53 61	anbi12d	$⊢ i = I \to ((X = [\forall_{𝑔} n (i \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 (X = [\forall_{𝑔} n (I \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
63	62	rexbidv	$⊢ i = I \to (\exists n \in ω (X = [\forall_{𝑔} n (i \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \exists n \in ω (X = [\forall_{𝑔} n (I \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
64	50 63	orbi12d	$⊢ i = I \to ((\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 (\exists k \in ω \exists l \in ω (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\})))$
65		oveq2	$⊢ j = J \to I \in_{𝑔} j = I \in_{𝑔} J$
66	65	oveq1d	$⊢ j = J \to (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l)$
67	66	eqeq2d	$⊢ j = J \to (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l))$
68		fveq2	$⊢ j = J \to a (j) = a (J)$
69	68	breq2d	$⊢ j = J \to (a (I) E a (j) \leftrightarrow a (I) E a (J))$
70	69	notbid	$⊢ j = J \to (\neg a (I) E a (j) \leftrightarrow \neg a (I) E a (J))$
71	70	orbi1d	$⊢ j = J \to ((\neg a (I) E a (j) \lor \neg a (k) E a (l)) \leftrightarrow (\neg a (I) E a (J) \lor \neg a (k) E a (l)))$
72	71	rabbidv	$⊢ j = J \to \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\}$
73	72	eqeq2d	$⊢ j = J \to (\{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\} \leftrightarrow \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\})$
74	67 73	anbi12d	$⊢ j = J \to ((X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\}) \leftrightarrow (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\}))$
75	74	2rexbidv	$⊢ j = J \to (\exists k \in ω \exists l \in ω (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (j) \lor \neg a (k) E a (l))\}) \leftrightarrow \exists k \in ω \exists l \in ω (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (k) E a (l))\}))$
76		eqidd	$⊢ j = J \to n = n$
77	76 65	goaleq12d	$⊢ j = J \to [\forall_{𝑔} n (I \in_{𝑔} j)] = [\forall_{𝑔} n (I \in_{𝑔} J)]$
78	77	eqeq2d	$⊢ j = J \to (X = [\forall_{𝑔} n (I \in_{𝑔} j)] \leftrightarrow X = [\forall_{𝑔} n (I \in_{𝑔} J)])$
79		eqeq1	$⊢ j = J \to (j = n \leftrightarrow J = n)$
80		biidd	$⊢ j = J \to (z E z \leftrightarrow z E z)$
81	68	breq2d	$⊢ j = J \to (z E a (j) \leftrightarrow z E a (J))$
82	79 80 81	ifpbi123d	$⊢ j = J \to (if- (j = n, z E z, z E a (j)) \leftrightarrow if- (J = n, z E z, z E a (J)))$
83		biidd	$⊢ j = J \to (a (I) E z \leftrightarrow a (I) E z)$
84	79 83 69	ifpbi123d	$⊢ j = J \to (if- (j = n, a (I) E z, a (I) E a (j)) \leftrightarrow if- (J = n, a (I) E z, a (I) E a (J)))$
85	82 84	ifpbi23d	$⊢ j = J \to (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 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))))$
86	85	ralbidv	$⊢ j = J \to (\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 \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))))$
87	86	rabbidv	$⊢ j = J \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 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)))\}$
88	87	eqeq2d	$⊢ j = J \to (\{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\})$
89	78 88	anbi12d	$⊢ j = J \to ((X = [\forall_{𝑔} n (I \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 (X = [\forall_{𝑔} n (I \in_{𝑔} J)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
90	89	rexbidv	$⊢ j = J \to (\exists n \in ω (X = [\forall_{𝑔} n (I \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \exists n \in ω (X = [\forall_{𝑔} n (I \in_{𝑔} J)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
91	75 90	orbi12d	$⊢ j = J \to ((\exists k \in ω \exists l \in ω (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 (\exists k \in ω \exists l \in ω (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\})))$
92	64 91	rspc2ev	$⊢ (I \in ω \land J \in ω \land (\exists k \in ω \exists l \in ω (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
93	10 11 39 92	syl3anc	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
94	1	ovexi	$⊢ X \in V$
95	94	a1i	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in V$
96		ovex	$⊢ M^{ω} \in V$
97	96	rabex	$⊢ \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} \in V$
98		eqeq1	$⊢ x = X \to (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
99		eqeq1	$⊢ y = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} \to (y = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\} \leftrightarrow \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\})$
100	98 99	bi2anan9	$⊢ (x = X \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 = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}) \leftrightarrow (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}))$
101	100	2rexbidv	$⊢ (x = X \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 ω (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))\}) \leftrightarrow \exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{a \in (M^{ω}) \| (\neg a (i) E a (j) \lor \neg a (k) E a (l))\}))$
102		eqeq1	$⊢ x = X \to (x = [\forall_{𝑔} n (i \in_{𝑔} j)] \leftrightarrow X = [\forall_{𝑔} n (i \in_{𝑔} j)])$
103		eqeq1	$⊢ y = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} \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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\})$
104	102 103	bi2anan9	$⊢ (x = X \land y = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}) \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)))\}) \leftrightarrow (X = [\forall_{𝑔} n (i \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
105	104	rexbidv	$⊢ (x = X \land y = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}) \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)))\}) \leftrightarrow \exists n \in ω (X = [\forall_{𝑔} n (i \in_{𝑔} j)] \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\}))$
106	101 105	orbi12d	$⊢ (x = X \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 ω (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)))\})) \leftrightarrow (\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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)))\})))$
107	106	2rexbidv	$⊢ (x = X \land y = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}) \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)))\})) \leftrightarrow \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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	107	opelopabga	$⊢ (X \in V \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} \in V) \to (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in \{⟨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)))\}))\} \leftrightarrow \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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	95 97 108	sylancl	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in \{⟨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)))\}))\} \leftrightarrow \exists i \in ω \exists j \in ω (\exists k \in ω \exists l \in ω (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \land \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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 \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\} = \{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	93 109	mpbird	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in \{⟨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)))\}))\}$
111	110	olcd	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in (M Sat E) (\emptyset) \lor ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in \{⟨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)))\}))\})$
112		elun	$⊢ ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in ((M Sat E) (\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)))\}))\}) \leftrightarrow (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in (M Sat E) (\emptyset) \lor ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in \{⟨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)))\}))\})$
113	111 112	sylibr	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in ((M Sat E) (\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)))\}))\})$
114		eqid	$⊢ M Sat E = M Sat E$
115	114	satfv1	$⊢ (M \in V \land E \in W) \to (M Sat E) (1_{𝑜}) = (M Sat E) (\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)))\}))\}$
116	115	eleq2d	$⊢ (M \in V \land E \in W) \to (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in (M Sat E) (1_{𝑜}) \leftrightarrow ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in ((M Sat E) (\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)))\}))\}))$
117	116	3ad2ant1	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in (M Sat E) (1_{𝑜}) \leftrightarrow ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in ((M Sat E) (\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)))\}))\}))$
118	113 117	mpbird	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to ⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in (M Sat E) (1_{𝑜})$
119		funopfv	$⊢ Fun (M Sat E) (1_{𝑜}) \to (⟨X, \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}⟩ \in (M Sat E) (1_{𝑜}) \to (M Sat E) (1_{𝑜}) (X) = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\})$
120	9 118 119	sylc	$⊢ ((M \in V \land E \in W) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat E) (1_{𝑜}) (X) = \{a \in (M^{ω}) \| (\neg a (I) E a (J) \lor \neg a (K) E a (L))\}$

Metamath Proof Explorer

Theorem satfv1fvfmla1

Proof