satfvsuclem1

		Ref	Expression
	Hypothesis	satfv0.s	$⊢ S = M Sat E$
	Assertion	satfvsuclem1	$⊢ (M \in V \land E \in W \land N \in ω) \to \{⟨x, y⟩ \| (\exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land y \in 𝒫 (M^{ω}))\} \in V$

Proof

Step	Hyp	Ref	Expression
1		satfv0.s	$⊢ S = M Sat E$
2		ancom	$⊢ (\exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land y \in 𝒫 (M^{ω})) \leftrightarrow (y \in 𝒫 (M^{ω}) \land \exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
3	2	opabbii	$⊢ \{⟨x, y⟩ \| (\exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land y \in 𝒫 (M^{ω}))\} = \{⟨x, y⟩ \| (y \in 𝒫 (M^{ω}) \land \exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))\}$
4		ovex	$⊢ M^{ω} \in V$
5	4	pwex	$⊢ 𝒫 (M^{ω}) \in V$
6	5	a1i	$⊢ (M \in V \land E \in W \land N \in ω) \to 𝒫 (M^{ω}) \in V$
7		fvex	$⊢ S (N) \in V$
8		unab	$⊢ \{x \| \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))\} \cup \{x \| \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})\} = \{x \| (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
9	7	abrexex	$⊢ \{x \| \exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)\} \in V$
10		simpl	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
11	10	reximi	$⊢ \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to \exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
12	11	ss2abi	$⊢ \{x \| \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))\} \subseteq \{x \| \exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)\}$
13	9 12	ssexi	$⊢ \{x \| \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))\} \in V$
14		omex	$⊢ ω \in V$
15	14	abrexex	$⊢ \{x \| \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]\} \in V$
16		simpl	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to x = [\forall_{𝑔} i 1^{st} (u)]$
17	16	reximi	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]$
18	17	ss2abi	$⊢ \{x \| \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})\} \subseteq \{x \| \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]\}$
19	15 18	ssexi	$⊢ \{x \| \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})\} \in V$
20	13 19	unex	$⊢ \{x \| \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))\} \cup \{x \| \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})\} \in V$
21	8 20	eqeltrri	$⊢ \{x \| (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \in V$
22	21	a1i	$⊢ (((M \in V \land E \in W \land N \in ω) \land y \in 𝒫 (M^{ω})) \land u \in S (N)) \to \{x \| (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \in V$
23	22	ralrimiva	$⊢ ((M \in V \land E \in W \land N \in ω) \land y \in 𝒫 (M^{ω})) \to \forall u \in S (N) \{x \| (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \in V$
24		abrexex2g	$⊢ (S (N) \in V \land \forall u \in S (N) \{x \| (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \in V) \to \{x \| \exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \in V$
25	7 23 24	sylancr	$⊢ ((M \in V \land E \in W \land N \in ω) \land y \in 𝒫 (M^{ω})) \to \{x \| \exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \in V$
26	6 25	opabex3rd	$⊢ (M \in V \land E \in W \land N \in ω) \to \{⟨x, y⟩ \| (y \in 𝒫 (M^{ω}) \land \exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))\} \in V$
27	3 26	eqeltrid	$⊢ (M \in V \land E \in W \land N \in ω) \to \{⟨x, y⟩ \| (\exists u \in S (N) (\exists v \in S (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \land y \in 𝒫 (M^{ω}))\} \in V$

Metamath Proof Explorer

Theorem satfvsuclem1

Proof