satffunlem1lem1

		Ref	Expression
	Assertion	satffunlem1lem1	$⊢ Fun (M Sat E) (N) \to Fun \{⟨x, y⟩ \| \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ u = s \to 1^{st} (u) = 1^{st} (s)$
2		fveq2	$⊢ v = r \to 1^{st} (v) = 1^{st} (r)$
3	1 2	oveqan12d	$⊢ (u = s \land v = r) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r)$
4	3	eqeq2d	$⊢ (u = s \land v = r) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r))$
5		fveq2	$⊢ u = s \to 2^{nd} (u) = 2^{nd} (s)$
6		fveq2	$⊢ v = r \to 2^{nd} (v) = 2^{nd} (r)$
7	5 6	ineqan12d	$⊢ (u = s \land v = r) \to 2^{nd} (u) \cap 2^{nd} (v) = 2^{nd} (s) \cap 2^{nd} (r)$
8	7	difeq2d	$⊢ (u = s \land v = r) \to (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))$
9	8	eqeq2d	$⊢ (u = s \land v = r) \to (y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))$
10	4 9	anbi12d	$⊢ (u = s \land v = r) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
11	10	cbvrexdva	$⊢ u = s \to (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists r \in (M Sat E) (N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))))$
12		simpr	$⊢ (u = s \land i = j) \to i = j$
13	1	adantr	$⊢ (u = s \land i = j) \to 1^{st} (u) = 1^{st} (s)$
14	12 13	goaleq12d	$⊢ (u = s \land i = j) \to [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)]$
15	14	eqeq2d	$⊢ (u = s \land i = j) \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} j 1^{st} (s)])$
16		opeq1	$⊢ i = j \to ⟨i, k⟩ = ⟨j, k⟩$
17	16	sneqd	$⊢ i = j \to \{⟨i, k⟩\} = \{⟨j, k⟩\}$
18		sneq	$⊢ i = j \to \{i\} = \{j\}$
19	18	difeq2d	$⊢ i = j \to ω ∖ \{i\} = ω ∖ \{j\}$
20	19	reseq2d	$⊢ i = j \to {f ↾}_{(ω ∖ \{i\})} = {f ↾}_{(ω ∖ \{j\})}$
21	17 20	uneq12d	$⊢ i = j \to \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) = \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})})$
22	21	adantl	$⊢ (u = s \land i = j) \to \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) = \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})})$
23	5	adantr	$⊢ (u = s \land i = j) \to 2^{nd} (u) = 2^{nd} (s)$
24	22 23	eleq12d	$⊢ (u = s \land i = j) \to (\{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u) \leftrightarrow \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s))$
25	24	ralbidv	$⊢ (u = s \land i = j) \to (\forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u) \leftrightarrow \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s))$
26	25	rabbidv	$⊢ (u = s \land i = j) \to \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}$
27	26	eqeq2d	$⊢ (u = s \land i = j) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})$
28	15 27	anbi12d	$⊢ (u = s \land i = j) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}))$
29	28	cbvrexdva	$⊢ u = s \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}))$
30	11 29	orbi12d	$⊢ u = s \to ((\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists r \in (M Sat E) (N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})))$
31	30	cbvrexvw	$⊢ \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists s \in (M Sat E) (N) (\exists r \in (M Sat E) (N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}))$
32		simp-4l	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \land v \in (M Sat E) (N)) \to Fun (M Sat E) (N)$
33		simpr	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \to u \in (M Sat E) (N)$
34	33	anim1i	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \land v \in (M Sat E) (N)) \to (u \in (M Sat E) (N) \land v \in (M Sat E) (N))$
35		simpr	$⊢ (Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \to s \in (M Sat E) (N)$
36	35	anim1i	$⊢ ((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \to (s \in (M Sat E) (N) \land r \in (M Sat E) (N))$
37	36	ad2antrr	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \land v \in (M Sat E) (N)) \to (s \in (M Sat E) (N) \land r \in (M Sat E) (N))$
38		satffunlem	$⊢ ((Fun (M Sat E) (N) \land (u \in (M Sat E) (N) \land v \in (M Sat E) (N)) \land (s \in (M Sat E) (N) \land r \in (M Sat E) (N))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to z = y$
39	38	eqcomd	$⊢ ((Fun (M Sat E) (N) \land (u \in (M Sat E) (N) \land v \in (M Sat E) (N)) \land (s \in (M Sat E) (N) \land r \in (M Sat E) (N))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)))) \to y = z$
40	39	3exp	$⊢ (Fun (M Sat E) (N) \land (u \in (M Sat E) (N) \land v \in (M Sat E) (N)) \land (s \in (M Sat E) (N) \land r \in (M Sat E) (N))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
41	32 34 37 40	syl3anc	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \land v \in (M Sat E) (N)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
42	41	rexlimdva	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \to (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
43		eqeq1	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \leftrightarrow [\forall_{𝑔} i 1^{st} (u)] = 1^{st} (s) ⊼_{𝑔} 1^{st} (r))$
44		df-goal	$⊢ [\forall_{𝑔} i 1^{st} (u)] = ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩$
45		fvex	$⊢ 1^{st} (s) \in V$
46		fvex	$⊢ 1^{st} (r) \in V$
47		gonafv	$⊢ (1^{st} (s) \in V \land 1^{st} (r) \in V) \to 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
48	45 46 47	mp2an	$⊢ 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
49	44 48	eqeq12i	$⊢ [\forall_{𝑔} i 1^{st} (u)] = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \leftrightarrow ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
50		2oex	$⊢ 2_{𝑜} \in V$
51		opex	$⊢ ⟨i, 1^{st} (u)⟩ \in V$
52	50 51	opth	$⊢ ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩ \leftrightarrow (2_{𝑜} = 1_{𝑜} \land ⟨i, 1^{st} (u)⟩ = ⟨1^{st} (s), 1^{st} (r)⟩)$
53		1one2o	$⊢ 1_{𝑜} \neq 2_{𝑜}$
54		df-ne	$⊢ 1_{𝑜} \neq 2_{𝑜} \leftrightarrow \neg 1_{𝑜} = 2_{𝑜}$
55		pm2.21	$⊢ \neg 1_{𝑜} = 2_{𝑜} \to (1_{𝑜} = 2_{𝑜} \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z))$
56	54 55	sylbi	$⊢ 1_{𝑜} \neq 2_{𝑜} \to (1_{𝑜} = 2_{𝑜} \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z))$
57	53 56	ax-mp	$⊢ 1_{𝑜} = 2_{𝑜} \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z)$
58	57	eqcoms	$⊢ 2_{𝑜} = 1_{𝑜} \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z)$
59	58	adantr	$⊢ (2_{𝑜} = 1_{𝑜} \land ⟨i, 1^{st} (u)⟩ = ⟨1^{st} (s), 1^{st} (r)⟩) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z)$
60	52 59	sylbi	$⊢ ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩ \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z)$
61	49 60	sylbi	$⊢ [\forall_{𝑔} i 1^{st} (u)] = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z)$
62	43 61	syl6bi	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to y = z))$
63	62	impd	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z)$
64	63	adantr	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z)$
65	64	a1i	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \land i \in ω) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
66	65	rexlimdva	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
67	42 66	jaod	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \land u \in (M Sat E) (N)) \to ((\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
68	67	rexlimdva	$⊢ ((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to y = z))$
69	68	com23	$⊢ ((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land r \in (M Sat E) (N)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
70	69	rexlimdva	$⊢ (Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \to (\exists r \in (M Sat E) (N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
71		eqeq1	$⊢ x = [\forall_{𝑔} j 1^{st} (s)] \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow [\forall_{𝑔} j 1^{st} (s)] = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
72		df-goal	$⊢ [\forall_{𝑔} j 1^{st} (s)] = ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩$
73		fvex	$⊢ 1^{st} (u) \in V$
74		fvex	$⊢ 1^{st} (v) \in V$
75		gonafv	$⊢ (1^{st} (u) \in V \land 1^{st} (v) \in V) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
76	73 74 75	mp2an	$⊢ 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
77	72 76	eqeq12i	$⊢ [\forall_{𝑔} j 1^{st} (s)] = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
78		opex	$⊢ ⟨j, 1^{st} (s)⟩ \in V$
79	50 78	opth	$⊢ ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \leftrightarrow (2_{𝑜} = 1_{𝑜} \land ⟨j, 1^{st} (s)⟩ = ⟨1^{st} (u), 1^{st} (v)⟩)$
80		pm2.21	$⊢ \neg 1_{𝑜} = 2_{𝑜} \to (1_{𝑜} = 2_{𝑜} \to y = z)$
81	54 80	sylbi	$⊢ 1_{𝑜} \neq 2_{𝑜} \to (1_{𝑜} = 2_{𝑜} \to y = z)$
82	53 81	ax-mp	$⊢ 1_{𝑜} = 2_{𝑜} \to y = z$
83	82	eqcoms	$⊢ 2_{𝑜} = 1_{𝑜} \to y = z$
84	83	adantr	$⊢ (2_{𝑜} = 1_{𝑜} \land ⟨j, 1^{st} (s)⟩ = ⟨1^{st} (u), 1^{st} (v)⟩) \to y = z$
85	79 84	sylbi	$⊢ ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \to y = z$
86	77 85	sylbi	$⊢ [\forall_{𝑔} j 1^{st} (s)] = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to y = z$
87	71 86	syl6bi	$⊢ x = [\forall_{𝑔} j 1^{st} (s)] \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to y = z)$
88	87	adantr	$⊢ (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to y = z)$
89	88	com12	$⊢ x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z)$
90	89	adantr	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z)$
91	90	a1i	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land v \in (M Sat E) (N)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z))$
92	91	rexlimdva	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \to (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z))$
93		eqeq1	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to (x = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)])$
94	44 72	eqeq12i	$⊢ [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩$
95	50 51	opth	$⊢ ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ = ⟨2_{𝑜}, ⟨j, 1^{st} (s)⟩⟩ \leftrightarrow (2_{𝑜} = 2_{𝑜} \land ⟨i, 1^{st} (u)⟩ = ⟨j, 1^{st} (s)⟩)$
96		vex	$⊢ i \in V$
97	96 73	opth	$⊢ ⟨i, 1^{st} (u)⟩ = ⟨j, 1^{st} (s)⟩ \leftrightarrow (i = j \land 1^{st} (u) = 1^{st} (s))$
98	97	anbi2i	$⊢ (2_{𝑜} = 2_{𝑜} \land ⟨i, 1^{st} (u)⟩ = ⟨j, 1^{st} (s)⟩) \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s)))$
99	94 95 98	3bitri	$⊢ [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s)))$
100	93 99	syl6bb	$⊢ x = [\forall_{𝑔} i 1^{st} (u)] \to (x = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))))$
101	100	adantl	$⊢ (((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to (x = [\forall_{𝑔} j 1^{st} (s)] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))))$
102		funfv1st2nd	$⊢ (Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \to (M Sat E) (N) (1^{st} (s)) = 2^{nd} (s)$
103	102	ex	$⊢ Fun (M Sat E) (N) \to (s \in (M Sat E) (N) \to (M Sat E) (N) (1^{st} (s)) = 2^{nd} (s))$
104		funfv1st2nd	$⊢ (Fun (M Sat E) (N) \land u \in (M Sat E) (N)) \to (M Sat E) (N) (1^{st} (u)) = 2^{nd} (u)$
105	104	ex	$⊢ Fun (M Sat E) (N) \to (u \in (M Sat E) (N) \to (M Sat E) (N) (1^{st} (u)) = 2^{nd} (u))$
106		fveqeq2	$⊢ 1^{st} (u) = 1^{st} (s) \to ((M Sat E) (N) (1^{st} (u)) = 2^{nd} (u) \leftrightarrow (M Sat E) (N) (1^{st} (s)) = 2^{nd} (u))$
107		eqtr2	$⊢ ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (u) \land (M Sat E) (N) (1^{st} (s)) = 2^{nd} (s)) \to 2^{nd} (u) = 2^{nd} (s)$
108		opeq1	$⊢ j = i \to ⟨j, k⟩ = ⟨i, k⟩$
109	108	sneqd	$⊢ j = i \to \{⟨j, k⟩\} = \{⟨i, k⟩\}$
110		sneq	$⊢ j = i \to \{j\} = \{i\}$
111	110	difeq2d	$⊢ j = i \to ω ∖ \{j\} = ω ∖ \{i\}$
112	111	reseq2d	$⊢ j = i \to {f ↾}_{(ω ∖ \{j\})} = {f ↾}_{(ω ∖ \{i\})}$
113	109 112	uneq12d	$⊢ j = i \to \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) = \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})})$
114	113	eqcoms	$⊢ i = j \to \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) = \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})})$
115	114	adantl	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) = \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})})$
116		simpl	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to 2^{nd} (u) = 2^{nd} (s)$
117	116	eqcomd	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to 2^{nd} (s) = 2^{nd} (u)$
118	115 117	eleq12d	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to (\{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s) \leftrightarrow \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u))$
119	118	ralbidv	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to (\forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s) \leftrightarrow \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u))$
120	119	rabbidv	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
121		eqeq12	$⊢ (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to (y = z \leftrightarrow \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
122	120 121	syl5ibrcom	$⊢ (2^{nd} (u) = 2^{nd} (s) \land i = j) \to ((y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to y = z)$
123	122	exp4b	$⊢ 2^{nd} (u) = 2^{nd} (s) \to (i = j \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
124	107 123	syl	$⊢ ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (u) \land (M Sat E) (N) (1^{st} (s)) = 2^{nd} (s)) \to (i = j \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
125	124	ex	$⊢ (M Sat E) (N) (1^{st} (s)) = 2^{nd} (u) \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to (i = j \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z))))$
126	106 125	syl6bi	$⊢ 1^{st} (u) = 1^{st} (s) \to ((M Sat E) (N) (1^{st} (u)) = 2^{nd} (u) \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to (i = j \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))))$
127	126	com24	$⊢ 1^{st} (u) = 1^{st} (s) \to (i = j \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to ((M Sat E) (N) (1^{st} (u)) = 2^{nd} (u) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))))$
128	127	impcom	$⊢ (i = j \land 1^{st} (u) = 1^{st} (s)) \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to ((M Sat E) (N) (1^{st} (u)) = 2^{nd} (u) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z))))$
129	128	com13	$⊢ (M Sat E) (N) (1^{st} (u)) = 2^{nd} (u) \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z))))$
130	105 129	syl6	$⊢ Fun (M Sat E) (N) \to (u \in (M Sat E) (N) \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))))$
131	130	com23	$⊢ Fun (M Sat E) (N) \to ((M Sat E) (N) (1^{st} (s)) = 2^{nd} (s) \to (u \in (M Sat E) (N) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))))$
132	103 131	syld	$⊢ Fun (M Sat E) (N) \to (s \in (M Sat E) (N) \to (u \in (M Sat E) (N) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))))$
133	132	imp	$⊢ (Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \to (u \in (M Sat E) (N) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z))))$
134	133	adantr	$⊢ ((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \to (u \in (M Sat E) (N) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z))))$
135	134	imp	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \to ((i = j \land 1^{st} (u) = 1^{st} (s)) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
136	135	adantld	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \to ((2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
137	136	ad2antrr	$⊢ (((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to ((2_{𝑜} = 2_{𝑜} \land (i = j \land 1^{st} (u) = 1^{st} (s))) \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
138	101 137	sylbid	$⊢ (((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to (x = [\forall_{𝑔} j 1^{st} (s)] \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\} \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
139	138	impd	$⊢ (((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \land x = [\forall_{𝑔} i 1^{st} (u)]) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z))$
140	139	ex	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to y = z)))$
141	140	com34	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to (z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z)))$
142	141	impd	$⊢ ((((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \land i \in ω) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z))$
143	142	rexlimdva	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z))$
144	92 143	jaod	$⊢ (((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \land u \in (M Sat E) (N)) \to ((\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z))$
145	144	rexlimdva	$⊢ ((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to y = z))$
146	145	com23	$⊢ ((Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \land j \in ω) \to ((x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
147	146	rexlimdva	$⊢ (Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \to (\exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\}) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
148	70 147	jaod	$⊢ (Fun (M Sat E) (N) \land s \in (M Sat E) (N)) \to ((\exists r \in (M Sat E) (N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
149	148	rexlimdva	$⊢ Fun (M Sat E) (N) \to (\exists s \in (M Sat E) (N) (\exists r \in (M Sat E) (N) (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \lor \exists j \in ω (x = [\forall_{𝑔} j 1^{st} (s)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨j, k⟩\} \cup ({f ↾}_{(ω ∖ \{j\})}) \in 2^{nd} (s)\})) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
150	31 149	syl5bi	$⊢ Fun (M Sat E) (N) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to y = z))$
151	150	impd	$⊢ Fun (M Sat E) (N) \to ((\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to y = z)$
152	151	alrimivv	$⊢ Fun (M Sat E) (N) \to \forall y \forall z ((\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to y = z)$
153		eqeq1	$⊢ y = z \to (y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
154	153	anbi2d	$⊢ y = z \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
155	154	rexbidv	$⊢ y = z \to (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
156		eqeq1	$⊢ y = z \to (y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
157	156	anbi2d	$⊢ y = z \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
158	157	rexbidv	$⊢ y = z \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
159	155 158	orbi12d	$⊢ y = z \to ((\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
160	159	rexbidv	$⊢ y = z \to (\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
161	160	mo4	$⊢ \exists^{*} y \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \forall y \forall z ((\exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land z = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land z = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to y = z)$
162	152 161	sylibr	$⊢ Fun (M Sat E) (N) \to \exists^{*} y \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
163	162	alrimiv	$⊢ Fun (M Sat E) (N) \to \forall x \exists^{*} y \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
164		funopab	$⊢ Fun \{⟨x, y⟩ \| \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \leftrightarrow \forall x \exists^{*} y \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
165	163 164	sylibr	$⊢ Fun (M Sat E) (N) \to Fun \{⟨x, y⟩ \| \exists u \in (M Sat E) (N) (\exists v \in (M Sat E) (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$

Metamath Proof Explorer

Theorem satffunlem1lem1

Proof