satffunlem1lem2

		Ref	Expression
	Assertion	satffunlem1lem2	$⊢ (M \in V \land E \in W) \to dom (M Sat E) (\emptyset) \cap dom \{⟨x, y⟩ \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) (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 j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2		satfdmfmla	$⊢ (M \in V \land E \in W \land \emptyset \in ω) \to dom (M Sat E) (\emptyset) = Fmla (\emptyset)$
3	1 2	mp3an3	$⊢ (M \in V \land E \in W) \to dom (M Sat E) (\emptyset) = Fmla (\emptyset)$
4		ovex	$⊢ M^{ω} \in V$
5	4	difexi	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V$
6	5	a1i	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land v \in (M Sat E) (\emptyset)) \to (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V$
7	6	ralrimiva	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to \forall v \in (M Sat E) (\emptyset) (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V$
8	4	rabex	$⊢ \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V$
9	8	a1i	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land i \in ω) \to \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V$
10	9	ralrimiva	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to \forall i \in ω \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V$
11	7 10	jca	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to (\forall v \in (M Sat E) (\emptyset) (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V \land \forall i \in ω \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V)$
12	11	ralrimiva	$⊢ (M \in V \land E \in W) \to \forall u \in (M Sat E) (\emptyset) (\forall v \in (M Sat E) (\emptyset) (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V \land \forall i \in ω \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V)$
13		dmopab2rex	$⊢ \forall u \in (M Sat E) (\emptyset) (\forall v \in (M Sat E) (\emptyset) (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V \land \forall i \in ω \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in V) \to dom \{⟨x, y⟩ \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) (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 j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{x \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
14	12 13	syl	$⊢ (M \in V \land E \in W) \to dom \{⟨x, y⟩ \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) (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 j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{x \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
15		satfrel	$⊢ (M \in V \land E \in W \land \emptyset \in ω) \to Rel (M Sat E) (\emptyset)$
16	1 15	mp3an3	$⊢ (M \in V \land E \in W) \to Rel (M Sat E) (\emptyset)$
17		1stdm	$⊢ (Rel (M Sat E) (\emptyset) \land u \in (M Sat E) (\emptyset)) \to 1^{st} (u) \in dom (M Sat E) (\emptyset)$
18	16 17	sylan	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to 1^{st} (u) \in dom (M Sat E) (\emptyset)$
19	2	eqcomd	$⊢ (M \in V \land E \in W \land \emptyset \in ω) \to Fmla (\emptyset) = dom (M Sat E) (\emptyset)$
20	1 19	mp3an3	$⊢ (M \in V \land E \in W) \to Fmla (\emptyset) = dom (M Sat E) (\emptyset)$
21	20	adantr	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to Fmla (\emptyset) = dom (M Sat E) (\emptyset)$
22	18 21	eleqtrrd	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to 1^{st} (u) \in Fmla (\emptyset)$
23	22	adantr	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to 1^{st} (u) \in Fmla (\emptyset)$
24		oveq1	$⊢ f = 1^{st} (u) \to f ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} g$
25	24	eqeq2d	$⊢ f = 1^{st} (u) \to (x = f ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} g)$
26	25	rexbidv	$⊢ f = 1^{st} (u) \to (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \leftrightarrow \exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g)$
27		eqidd	$⊢ f = 1^{st} (u) \to i = i$
28		id	$⊢ f = 1^{st} (u) \to f = 1^{st} (u)$
29	27 28	goaleq12d	$⊢ f = 1^{st} (u) \to [\forall_{𝑔} i f] = [\forall_{𝑔} i 1^{st} (u)]$
30	29	eqeq2d	$⊢ f = 1^{st} (u) \to (x = [\forall_{𝑔} i f] \leftrightarrow x = [\forall_{𝑔} i 1^{st} (u)])$
31	30	rexbidv	$⊢ f = 1^{st} (u) \to (\exists i \in ω x = [\forall_{𝑔} i f] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
32	26 31	orbi12d	$⊢ f = 1^{st} (u) \to ((\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \leftrightarrow (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
33	32	adantl	$⊢ ((((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \land f = 1^{st} (u)) \to ((\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \leftrightarrow (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
34		1stdm	$⊢ (Rel (M Sat E) (\emptyset) \land v \in (M Sat E) (\emptyset)) \to 1^{st} (v) \in dom (M Sat E) (\emptyset)$
35	16 34	sylan	$⊢ ((M \in V \land E \in W) \land v \in (M Sat E) (\emptyset)) \to 1^{st} (v) \in dom (M Sat E) (\emptyset)$
36	20	adantr	$⊢ ((M \in V \land E \in W) \land v \in (M Sat E) (\emptyset)) \to Fmla (\emptyset) = dom (M Sat E) (\emptyset)$
37	35 36	eleqtrrd	$⊢ ((M \in V \land E \in W) \land v \in (M Sat E) (\emptyset)) \to 1^{st} (v) \in Fmla (\emptyset)$
38	37	ad4ant13	$⊢ ((((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land v \in (M Sat E) (\emptyset)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to 1^{st} (v) \in Fmla (\emptyset)$
39		oveq2	$⊢ g = 1^{st} (v) \to 1^{st} (u) ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
40	39	eqeq2d	$⊢ g = 1^{st} (v) \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
41	40	adantl	$⊢ (((((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land v \in (M Sat E) (\emptyset)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \land g = 1^{st} (v)) \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
42		simpr	$⊢ ((((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land v \in (M Sat E) (\emptyset)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
43	38 41 42	rspcedvd	$⊢ ((((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land v \in (M Sat E) (\emptyset)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to \exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g$
44	43	ex	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land v \in (M Sat E) (\emptyset)) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g)$
45	44	rexlimdva	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g)$
46	45	orim1d	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to ((\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
47	46	imp	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
48	23 33 47	rspcedvd	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])$
49	48	ex	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to ((\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
50	49	rexlimdva	$⊢ (M \in V \land E \in W) \to (\exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
51		releldm2	$⊢ Rel (M Sat E) (\emptyset) \to (f \in dom (M Sat E) (\emptyset) \leftrightarrow \exists u \in (M Sat E) (\emptyset) 1^{st} (u) = f)$
52	16 51	syl	$⊢ (M \in V \land E \in W) \to (f \in dom (M Sat E) (\emptyset) \leftrightarrow \exists u \in (M Sat E) (\emptyset) 1^{st} (u) = f)$
53	3	eleq2d	$⊢ (M \in V \land E \in W) \to (f \in dom (M Sat E) (\emptyset) \leftrightarrow f \in Fmla (\emptyset))$
54	52 53	bitr3d	$⊢ (M \in V \land E \in W) \to (\exists u \in (M Sat E) (\emptyset) 1^{st} (u) = f \leftrightarrow f \in Fmla (\emptyset))$
55		r19.41v	$⊢ \exists u \in (M Sat E) (\emptyset) (1^{st} (u) = f \land (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \leftrightarrow (\exists u \in (M Sat E) (\emptyset) 1^{st} (u) = f \land (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
56		oveq1	$⊢ 1^{st} (u) = f \to 1^{st} (u) ⊼_{𝑔} g = f ⊼_{𝑔} g$
57	56	eqeq2d	$⊢ 1^{st} (u) = f \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = f ⊼_{𝑔} g)$
58	57	rexbidv	$⊢ 1^{st} (u) = f \to (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow \exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g)$
59		eqidd	$⊢ 1^{st} (u) = f \to i = i$
60		id	$⊢ 1^{st} (u) = f \to 1^{st} (u) = f$
61	59 60	goaleq12d	$⊢ 1^{st} (u) = f \to [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} i f]$
62	61	eqeq2d	$⊢ 1^{st} (u) = f \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} i f])$
63	62	rexbidv	$⊢ 1^{st} (u) = f \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i f])$
64	58 63	orbi12d	$⊢ 1^{st} (u) = f \to ((\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
65	64	adantl	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land 1^{st} (u) = f) \to ((\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
66	3	eqcomd	$⊢ (M \in V \land E \in W) \to Fmla (\emptyset) = dom (M Sat E) (\emptyset)$
67	66	eleq2d	$⊢ (M \in V \land E \in W) \to (g \in Fmla (\emptyset) \leftrightarrow g \in dom (M Sat E) (\emptyset))$
68		releldm2	$⊢ Rel (M Sat E) (\emptyset) \to (g \in dom (M Sat E) (\emptyset) \leftrightarrow \exists v \in (M Sat E) (\emptyset) 1^{st} (v) = g)$
69	16 68	syl	$⊢ (M \in V \land E \in W) \to (g \in dom (M Sat E) (\emptyset) \leftrightarrow \exists v \in (M Sat E) (\emptyset) 1^{st} (v) = g)$
70	67 69	bitrd	$⊢ (M \in V \land E \in W) \to (g \in Fmla (\emptyset) \leftrightarrow \exists v \in (M Sat E) (\emptyset) 1^{st} (v) = g)$
71		r19.41v	$⊢ \exists v \in (M Sat E) (\emptyset) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \leftrightarrow (\exists v \in (M Sat E) (\emptyset) 1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g)$
72	39	eqcoms	$⊢ 1^{st} (v) = g \to 1^{st} (u) ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
73	72	eqeq2d	$⊢ 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
74	73	biimpa	$⊢ (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
75	74	a1i	$⊢ (M \in V \land E \in W) \to ((1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
76	75	reximdv	$⊢ (M \in V \land E \in W) \to (\exists v \in (M Sat E) (\emptyset) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
77	71 76	syl5bir	$⊢ (M \in V \land E \in W) \to ((\exists v \in (M Sat E) (\emptyset) 1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
78	77	expd	$⊢ (M \in V \land E \in W) \to (\exists v \in (M Sat E) (\emptyset) 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
79	70 78	sylbid	$⊢ (M \in V \land E \in W) \to (g \in Fmla (\emptyset) \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
80	79	rexlimdv	$⊢ (M \in V \land E \in W) \to (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
81	80	adantr	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
82	81	adantr	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land 1^{st} (u) = f) \to (\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
83	82	orim1d	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land 1^{st} (u) = f) \to ((\exists g \in Fmla (\emptyset) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
84	65 83	sylbird	$⊢ (((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \land 1^{st} (u) = f) \to ((\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
85	84	expimpd	$⊢ ((M \in V \land E \in W) \land u \in (M Sat E) (\emptyset)) \to ((1^{st} (u) = f \land (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \to (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
86	85	reximdva	$⊢ (M \in V \land E \in W) \to (\exists u \in (M Sat E) (\emptyset) (1^{st} (u) = f \land (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \to \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
87	55 86	syl5bir	$⊢ (M \in V \land E \in W) \to ((\exists u \in (M Sat E) (\emptyset) 1^{st} (u) = f \land (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \to \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
88	87	expd	$⊢ (M \in V \land E \in W) \to (\exists u \in (M Sat E) (\emptyset) 1^{st} (u) = f \to ((\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
89	54 88	sylbird	$⊢ (M \in V \land E \in W) \to (f \in Fmla (\emptyset) \to ((\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
90	89	rexlimdv	$⊢ (M \in V \land E \in W) \to (\exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
91	50 90	impbid	$⊢ (M \in V \land E \in W) \to (\exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
92	91	abbidv	$⊢ (M \in V \land E \in W) \to \{x \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} = \{x \| \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])\}$
93	14 92	eqtrd	$⊢ (M \in V \land E \in W) \to dom \{⟨x, y⟩ \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) (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 j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{x \| \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])\}$
94	3 93	ineq12d	$⊢ (M \in V \land E \in W) \to dom (M Sat E) (\emptyset) \cap dom \{⟨x, y⟩ \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) (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 j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = Fmla (\emptyset) \cap \{x \| \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])\}$
95		fmla0disjsuc	$⊢ Fmla (\emptyset) \cap \{x \| \exists f \in Fmla (\emptyset) (\exists g \in Fmla (\emptyset) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])\} = \emptyset$
96	94 95	eqtrdi	$⊢ (M \in V \land E \in W) \to dom (M Sat E) (\emptyset) \cap dom \{⟨x, y⟩ \| \exists u \in (M Sat E) (\emptyset) (\exists v \in (M Sat E) (\emptyset) (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 j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \emptyset$

Metamath Proof Explorer

Theorem satffunlem1lem2

Proof