satfdm

Description: The domain of the satisfaction predicate as function over wff codes does not depend on the model M and the binary relation E on M . (Contributed by AV, 13-Oct-2023)

		Ref	Expression
	Assertion	satfdm	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to \forall n \in ω dom (M Sat E) (n) = dom (N Sat F) (n)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = \emptyset \to (M Sat E) (x) = (M Sat E) (\emptyset)$
2	1	dmeqd	$⊢ x = \emptyset \to dom (M Sat E) (x) = dom (M Sat E) (\emptyset)$
3		fveq2	$⊢ x = \emptyset \to (N Sat F) (x) = (N Sat F) (\emptyset)$
4	3	dmeqd	$⊢ x = \emptyset \to dom (N Sat F) (x) = dom (N Sat F) (\emptyset)$
5	2 4	eqeq12d	$⊢ x = \emptyset \to (dom (M Sat E) (x) = dom (N Sat F) (x) \leftrightarrow dom (M Sat E) (\emptyset) = dom (N Sat F) (\emptyset))$
6	5	imbi2d	$⊢ x = \emptyset \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (x) = dom (N Sat F) (x)) \leftrightarrow (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (\emptyset) = dom (N Sat F) (\emptyset)))$
7		fveq2	$⊢ x = y \to (M Sat E) (x) = (M Sat E) (y)$
8	7	dmeqd	$⊢ x = y \to dom (M Sat E) (x) = dom (M Sat E) (y)$
9		fveq2	$⊢ x = y \to (N Sat F) (x) = (N Sat F) (y)$
10	9	dmeqd	$⊢ x = y \to dom (N Sat F) (x) = dom (N Sat F) (y)$
11	8 10	eqeq12d	$⊢ x = y \to (dom (M Sat E) (x) = dom (N Sat F) (x) \leftrightarrow dom (M Sat E) (y) = dom (N Sat F) (y))$
12	11	imbi2d	$⊢ x = y \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (x) = dom (N Sat F) (x)) \leftrightarrow (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)))$
13		fveq2	$⊢ x = suc y \to (M Sat E) (x) = (M Sat E) (suc y)$
14	13	dmeqd	$⊢ x = suc y \to dom (M Sat E) (x) = dom (M Sat E) (suc y)$
15		fveq2	$⊢ x = suc y \to (N Sat F) (x) = (N Sat F) (suc y)$
16	15	dmeqd	$⊢ x = suc y \to dom (N Sat F) (x) = dom (N Sat F) (suc y)$
17	14 16	eqeq12d	$⊢ x = suc y \to (dom (M Sat E) (x) = dom (N Sat F) (x) \leftrightarrow dom (M Sat E) (suc y) = dom (N Sat F) (suc y))$
18	17	imbi2d	$⊢ x = suc y \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (x) = dom (N Sat F) (x)) \leftrightarrow (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (suc y) = dom (N Sat F) (suc y)))$
19		fveq2	$⊢ x = n \to (M Sat E) (x) = (M Sat E) (n)$
20	19	dmeqd	$⊢ x = n \to dom (M Sat E) (x) = dom (M Sat E) (n)$
21		fveq2	$⊢ x = n \to (N Sat F) (x) = (N Sat F) (n)$
22	21	dmeqd	$⊢ x = n \to dom (N Sat F) (x) = dom (N Sat F) (n)$
23	20 22	eqeq12d	$⊢ x = n \to (dom (M Sat E) (x) = dom (N Sat F) (x) \leftrightarrow dom (M Sat E) (n) = dom (N Sat F) (n))$
24	23	imbi2d	$⊢ x = n \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (x) = dom (N Sat F) (x)) \leftrightarrow (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (n) = dom (N Sat F) (n)))$
25		rexcom4	$⊢ \exists v \in ω \exists y (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists y \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})$
26	25	rexbii	$⊢ \exists u \in ω \exists v \in ω \exists y (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists u \in ω \exists y \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})$
27		ovex	$⊢ M^{ω} \in V$
28	27	rabex	$⊢ \{a \in (M^{ω}) \| a (u) E a (v)\} \in V$
29	28	isseti	$⊢ \exists y y = \{a \in (M^{ω}) \| a (u) E a (v)\}$
30		ovex	$⊢ N^{ω} \in V$
31	30	rabex	$⊢ \{a \in (N^{ω}) \| a (u) F a (v)\} \in V$
32	31	isseti	$⊢ \exists z z = \{a \in (N^{ω}) \| a (u) F a (v)\}$
33	29 32	2th	$⊢ \exists y y = \{a \in (M^{ω}) \| a (u) E a (v)\} \leftrightarrow \exists z z = \{a \in (N^{ω}) \| a (u) F a (v)\}$
34	33	anbi2i	$⊢ (x = u \in_{𝑔} v \land \exists y y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow (x = u \in_{𝑔} v \land \exists z z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
35		19.42v	$⊢ \exists y (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow (x = u \in_{𝑔} v \land \exists y y = \{a \in (M^{ω}) \| a (u) E a (v)\})$
36		19.42v	$⊢ \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\}) \leftrightarrow (x = u \in_{𝑔} v \land \exists z z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
37	34 35 36	3bitr4i	$⊢ \exists y (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
38	37	rexbii	$⊢ \exists v \in ω \exists y (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists v \in ω \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
39	38	rexbii	$⊢ \exists u \in ω \exists v \in ω \exists y (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists u \in ω \exists v \in ω \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
40		rexcom4	$⊢ \exists u \in ω \exists y \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})$
41	26 39 40	3bitr3ri	$⊢ \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists u \in ω \exists v \in ω \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
42		rexcom4	$⊢ \exists v \in ω \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\}) \leftrightarrow \exists z \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
43	42	rexbii	$⊢ \exists u \in ω \exists v \in ω \exists z (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\}) \leftrightarrow \exists u \in ω \exists z \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
44	41 43	bitri	$⊢ \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists u \in ω \exists z \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
45		rexcom4	$⊢ \exists u \in ω \exists z \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\}) \leftrightarrow \exists z \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
46	44 45	bitri	$⊢ \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\}) \leftrightarrow \exists z \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})$
47	46	abbii	$⊢ \{x \| \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\} = \{x \| \exists z \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\}$
48		eqid	$⊢ M Sat E = M Sat E$
49	48	satfv0	$⊢ (M \in V \land E \in W) \to (M Sat E) (\emptyset) = \{⟨x, y⟩ \| \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\}$
50	49	dmeqd	$⊢ (M \in V \land E \in W) \to dom (M Sat E) (\emptyset) = dom \{⟨x, y⟩ \| \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\}$
51		dmopab	$⊢ dom \{⟨x, y⟩ \| \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\} = \{x \| \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\}$
52	50 51	eqtrdi	$⊢ (M \in V \land E \in W) \to dom (M Sat E) (\emptyset) = \{x \| \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\}$
53	52	adantr	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (\emptyset) = \{x \| \exists y \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land y = \{a \in (M^{ω}) \| a (u) E a (v)\})\}$
54		eqid	$⊢ N Sat F = N Sat F$
55	54	satfv0	$⊢ (N \in X \land F \in Y) \to (N Sat F) (\emptyset) = \{⟨x, z⟩ \| \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\}$
56	55	dmeqd	$⊢ (N \in X \land F \in Y) \to dom (N Sat F) (\emptyset) = dom \{⟨x, z⟩ \| \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\}$
57		dmopab	$⊢ dom \{⟨x, z⟩ \| \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\} = \{x \| \exists z \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\}$
58	56 57	eqtrdi	$⊢ (N \in X \land F \in Y) \to dom (N Sat F) (\emptyset) = \{x \| \exists z \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\}$
59	58	adantl	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (N Sat F) (\emptyset) = \{x \| \exists z \exists u \in ω \exists v \in ω (x = u \in_{𝑔} v \land z = \{a \in (N^{ω}) \| a (u) F a (v)\})\}$
60	47 53 59	3eqtr4a	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (\emptyset) = dom (N Sat F) (\emptyset)$
61		pm2.27	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (y) = dom (N Sat F) (y))$
62	61	adantl	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (y) = dom (N Sat F) (y))$
63		simpr	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)$
64		simprl	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (M \in V \land E \in W)$
65		simpl	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to y \in ω$
66		df-3an	$⊢ (M \in V \land E \in W \land y \in ω) \leftrightarrow ((M \in V \land E \in W) \land y \in ω)$
67	64 65 66	sylanbrc	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (M \in V \land E \in W \land y \in ω)$
68		satfdmlem	$⊢ ((M \in V \land E \in W \land y \in ω) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (\exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]))$
69	67 68	sylan	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (\exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]))$
70		simprr	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (N \in X \land F \in Y)$
71		df-3an	$⊢ (N \in X \land F \in Y \land y \in ω) \leftrightarrow ((N \in X \land F \in Y) \land y \in ω)$
72	70 65 71	sylanbrc	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (N \in X \land F \in Y \land y \in ω)$
73		id	$⊢ dom (M Sat E) (y) = dom (N Sat F) (y) \to dom (M Sat E) (y) = dom (N Sat F) (y)$
74	73	eqcomd	$⊢ dom (M Sat E) (y) = dom (N Sat F) (y) \to dom (N Sat F) (y) = dom (M Sat E) (y)$
75		satfdmlem	$⊢ ((N \in X \land F \in Y \land y \in ω) \land dom (N Sat F) (y) = dom (M Sat E) (y)) \to (\exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]) \to \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
76	72 74 75	syl2an	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (\exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]) \to \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
77	69 76	impbid	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (\exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]))$
78	27	difexi	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V$
79	78	isseti	$⊢ \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
80	79	biantru	$⊢ x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
81	80	bicomi	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
82	81	rexbii	$⊢ \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
83	27	rabex	$⊢ \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V$
84	83	isseti	$⊢ \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
85	84	biantru	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
86	85	bicomi	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow x = [\forall_{𝑔} i 1^{st} (u)]$
87	86	rexbii	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]$
88	82 87	orbi12i	$⊢ (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
89	88	rexbii	$⊢ \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
90	30	difexi	$⊢ (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)) \in V$
91	90	isseti	$⊢ \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))$
92	91	biantru	$⊢ x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \leftrightarrow (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)))$
93	92	bicomi	$⊢ (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)$
94	93	rexbii	$⊢ \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow \exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)$
95	30	rabex	$⊢ \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\} \in V$
96	95	isseti	$⊢ \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}$
97	96	biantru	$⊢ x = [\forall_{𝑔} i 1^{st} (a)] \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})$
98	97	bicomi	$⊢ (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow x = [\forall_{𝑔} i 1^{st} (a)]$
99	98	rexbii	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]$
100	94 99	orbi12i	$⊢ (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)])$
101	100	rexbii	$⊢ \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)])$
102	77 89 101	3bitr4g	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (\exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})))$
103		19.42v	$⊢ \exists w (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
104	103	bicomi	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists w (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
105	104	rexbii	$⊢ \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in (M Sat E) (y) \exists w (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
106		rexcom4	$⊢ \exists v \in (M Sat E) (y) \exists w (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists w \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
107	105 106	bitri	$⊢ \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists w \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
108		19.42v	$⊢ \exists w (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
109	108	bicomi	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists w (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
110	109	rexbii	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists i \in ω \exists w (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
111		rexcom4	$⊢ \exists i \in ω \exists w (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists w \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
112	110 111	bitri	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists w \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
113	107 112	orbi12i	$⊢ (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists w \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists w \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
114		19.43	$⊢ \exists w (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists w \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists w \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
115	114	bicomi	$⊢ (\exists w \exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists w \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists w (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
116	113 115	bitri	$⊢ (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists w (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
117	116	rexbii	$⊢ \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in (M Sat E) (y) \exists w (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
118		rexcom4	$⊢ \exists u \in (M Sat E) (y) \exists w (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists w \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
119	117 118	bitri	$⊢ \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land \exists w w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land \exists w w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists w \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
120		19.42v	$⊢ \exists z (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)))$
121	120	bicomi	$⊢ (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow \exists z (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)))$
122	121	rexbii	$⊢ \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow \exists b \in (N Sat F) (y) \exists z (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)))$
123		rexcom4	$⊢ \exists b \in (N Sat F) (y) \exists z (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow \exists z \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)))$
124	122 123	bitri	$⊢ \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \leftrightarrow \exists z \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b)))$
125		19.42v	$⊢ \exists z (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})$
126	125	bicomi	$⊢ (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow \exists z (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})$
127	126	rexbii	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow \exists i \in ω \exists z (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})$
128		rexcom4	$⊢ \exists i \in ω \exists z (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow \exists z \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})$
129	127 128	bitri	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}) \leftrightarrow \exists z \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})$
130	124 129	orbi12i	$⊢ (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow (\exists z \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists z \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
131		19.43	$⊢ \exists z (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow (\exists z \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists z \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
132	131	bicomi	$⊢ (\exists z \exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists z \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow \exists z (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
133	130 132	bitri	$⊢ (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow \exists z (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
134	133	rexbii	$⊢ \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow \exists a \in (N Sat F) (y) \exists z (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
135		rexcom4	$⊢ \exists a \in (N Sat F) (y) \exists z (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow \exists z \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
136	134 135	bitri	$⊢ \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land \exists z z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land \exists z z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})) \leftrightarrow \exists z \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))$
137	102 119 136	3bitr3g	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (\exists w \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists z \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\})))$
138	137	abbidv	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to \{x \| \exists w \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{x \| \exists z \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
139		dmopab	$⊢ dom \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{x \| \exists w \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
140		dmopab	$⊢ dom \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\} = \{x \| \exists z \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
141	138 139 140	3eqtr4g	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = dom \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
142	63 141	uneq12d	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (y) \cup dom \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = dom (N Sat F) (y) \cup dom \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
143		dmun	$⊢ dom ((M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) = dom (M Sat E) (y) \cup dom \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
144		dmun	$⊢ dom ((N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}) = dom (N Sat F) (y) \cup dom \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
145	142 143 144	3eqtr4g	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom ((M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) = dom ((N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\})$
146		simpl	$⊢ (M \in V \land E \in W) \to M \in V$
147	146	adantr	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to M \in V$
148		simpr	$⊢ (M \in V \land E \in W) \to E \in W$
149	148	adantr	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to E \in W$
150	48	satfvsuc	$⊢ (M \in V \land E \in W \land y \in ω) \to (M Sat E) (suc y) = (M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
151	147 149 65 150	syl2an23an	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (M Sat E) (suc y) = (M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
152	151	dmeqd	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to dom (M Sat E) (suc y) = dom ((M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
153		simprl	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to N \in X$
154		simprr	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to F \in Y$
155	54	satfvsuc	$⊢ (N \in X \land F \in Y \land y \in ω) \to (N Sat F) (suc y) = (N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
156	153 154 65 155	syl2an23an	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (N Sat F) (suc y) = (N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}$
157	156	dmeqd	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to dom (N Sat F) (suc y) = dom ((N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\})$
158	152 157	eqeq12d	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (dom (M Sat E) (suc y) = dom (N Sat F) (suc y) \leftrightarrow dom ((M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) = dom ((N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}))$
159	158	adantr	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to (dom (M Sat E) (suc y) = dom (N Sat F) (suc y) \leftrightarrow dom ((M Sat E) (y) \cup \{⟨x, w⟩ \| \exists u \in (M Sat E) (y) (\exists v \in (M Sat E) (y) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land w = \{m \in (M^{ω}) \| \forall f \in M \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) = dom ((N Sat F) (y) \cup \{⟨x, z⟩ \| \exists a \in (N Sat F) (y) (\exists b \in (N Sat F) (y) (x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \land z = (N^{ω}) ∖ (2^{nd} (a) \cap 2^{nd} (b))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (a)] \land z = \{m \in (N^{ω}) \| \forall f \in N \{⟨i, f⟩\} \cup ({m ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (a)\}))\}))$
160	145 159	mpbird	$⊢ ((y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \land dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (suc y) = dom (N Sat F) (suc y)$
161	160	ex	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to (dom (M Sat E) (y) = dom (N Sat F) (y) \to dom (M Sat E) (suc y) = dom (N Sat F) (suc y))$
162	62 161	syld	$⊢ (y \in ω \land ((M \in V \land E \in W) \land (N \in X \land F \in Y))) \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (suc y) = dom (N Sat F) (suc y))$
163	162	ex	$⊢ y \in ω \to (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)) \to dom (M Sat E) (suc y) = dom (N Sat F) (suc y)))$
164	163	com23	$⊢ y \in ω \to ((((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (y) = dom (N Sat F) (y)) \to (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (suc y) = dom (N Sat F) (suc y)))$
165	6 12 18 24 60 164	finds	$⊢ n \in ω \to (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to dom (M Sat E) (n) = dom (N Sat F) (n))$
166	165	impcom	$⊢ (((M \in V \land E \in W) \land (N \in X \land F \in Y)) \land n \in ω) \to dom (M Sat E) (n) = dom (N Sat F) (n)$
167	166	ralrimiva	$⊢ ((M \in V \land E \in W) \land (N \in X \land F \in Y)) \to \forall n \in ω dom (M Sat E) (n) = dom (N Sat F) (n)$

Metamath Proof Explorer

Theorem satfdm

Proof