satfdmlem

		Ref	Expression
	Assertion	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)]))$

Proof

Step	Hyp	Ref	Expression
1		satfrel	$⊢ (M \in V \land E \in W \land Y \in ω) \to Rel (M Sat E) (Y)$
2	1	adantr	$⊢ ((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \to Rel (M Sat E) (Y)$
3		1stdm	$⊢ (Rel (M Sat E) (Y) \land u \in (M Sat E) (Y)) \to 1^{st} (u) \in dom (M Sat E) (Y)$
4	2 3	sylan	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to 1^{st} (u) \in dom (M Sat E) (Y)$
5		eleq2	$⊢ dom (M Sat E) (Y) = dom (N Sat F) (Y) \to (1^{st} (u) \in dom (M Sat E) (Y) \leftrightarrow 1^{st} (u) \in dom (N Sat F) (Y))$
6	5	adantl	$⊢ ((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \to (1^{st} (u) \in dom (M Sat E) (Y) \leftrightarrow 1^{st} (u) \in dom (N Sat F) (Y))$
7	6	adantr	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to (1^{st} (u) \in dom (M Sat E) (Y) \leftrightarrow 1^{st} (u) \in dom (N Sat F) (Y))$
8		fvex	$⊢ 1^{st} (u) \in V$
9		eldm2g	$⊢ 1^{st} (u) \in V \to (1^{st} (u) \in dom (N Sat F) (Y) \leftrightarrow \exists s ⟨1^{st} (u), s⟩ \in (N Sat F) (Y))$
10	8 9	ax-mp	$⊢ 1^{st} (u) \in dom (N Sat F) (Y) \leftrightarrow \exists s ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)$
11		simpr	$⊢ ((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \to ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)$
12	2	ad4antr	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to Rel (M Sat E) (Y)$
13		1stdm	$⊢ (Rel (M Sat E) (Y) \land v \in (M Sat E) (Y)) \to 1^{st} (v) \in dom (M Sat E) (Y)$
14	12 13	sylancom	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to 1^{st} (v) \in dom (M Sat E) (Y)$
15		eleq2	$⊢ dom (M Sat E) (Y) = dom (N Sat F) (Y) \to (1^{st} (v) \in dom (M Sat E) (Y) \leftrightarrow 1^{st} (v) \in dom (N Sat F) (Y))$
16	15	ad5antlr	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to (1^{st} (v) \in dom (M Sat E) (Y) \leftrightarrow 1^{st} (v) \in dom (N Sat F) (Y))$
17		fvex	$⊢ 1^{st} (v) \in V$
18		eldm2g	$⊢ 1^{st} (v) \in V \to (1^{st} (v) \in dom (N Sat F) (Y) \leftrightarrow \exists r ⟨1^{st} (v), r⟩ \in (N Sat F) (Y))$
19	17 18	ax-mp	$⊢ 1^{st} (v) \in dom (N Sat F) (Y) \leftrightarrow \exists r ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)$
20		simpr	$⊢ (((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \land ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)) \to ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)$
21		vex	$⊢ s \in V$
22	8 21	op1std	$⊢ a = ⟨1^{st} (u), s⟩ \to 1^{st} (a) = 1^{st} (u)$
23	22	eqcomd	$⊢ a = ⟨1^{st} (u), s⟩ \to 1^{st} (u) = 1^{st} (a)$
24	23	ad3antlr	$⊢ (((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \land ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)) \to 1^{st} (u) = 1^{st} (a)$
25		vex	$⊢ r \in V$
26	17 25	op1std	$⊢ b = ⟨1^{st} (v), r⟩ \to 1^{st} (b) = 1^{st} (v)$
27	26	eqcomd	$⊢ b = ⟨1^{st} (v), r⟩ \to 1^{st} (v) = 1^{st} (b)$
28	24 27	oveqan12d	$⊢ ((((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \land ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)) \land b = ⟨1^{st} (v), r⟩) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)$
29	28	eqeq2d	$⊢ ((((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \land ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)) \land b = ⟨1^{st} (v), r⟩) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b))$
30	29	biimpd	$⊢ ((((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \land ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)) \land b = ⟨1^{st} (v), r⟩) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b))$
31	20 30	rspcimedv	$⊢ (((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \land ⟨1^{st} (v), r⟩ \in (N Sat F) (Y)) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b))$
32	31	ex	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to (⟨1^{st} (v), r⟩ \in (N Sat F) (Y) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)))$
33	32	exlimdv	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to (\exists r ⟨1^{st} (v), r⟩ \in (N Sat F) (Y) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)))$
34	19 33	syl5bi	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to (1^{st} (v) \in dom (N Sat F) (Y) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)))$
35	16 34	sylbid	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to (1^{st} (v) \in dom (M Sat E) (Y) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b)))$
36	14 35	mpd	$⊢ ((((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \land v \in (M Sat E) (Y)) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b))$
37	36	rexlimdva	$⊢ (((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \to (\exists v \in (M Sat E) (Y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b))$
38		eqidd	$⊢ a = ⟨1^{st} (u), s⟩ \to i = i$
39	38 23	goaleq12d	$⊢ a = ⟨1^{st} (u), s⟩ \to [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} i 1^{st} (a)]$
40	39	eqeq2d	$⊢ a = ⟨1^{st} (u), s⟩ \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} i 1^{st} (a)])$
41	40	biimpd	$⊢ a = ⟨1^{st} (u), s⟩ \to (x = [\forall_{𝑔} i 1^{st} (u)] \to x = [\forall_{𝑔} i 1^{st} (a)])$
42	41	adantl	$⊢ (((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \to (x = [\forall_{𝑔} i 1^{st} (u)] \to x = [\forall_{𝑔} i 1^{st} (a)])$
43	42	reximdv	$⊢ (((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \to \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)])$
44	37 43	orim12d	$⊢ (((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \land a = ⟨1^{st} (u), s⟩) \to ((\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 b \in (N Sat F) (Y) x = 1^{st} (a) ⊼_{𝑔} 1^{st} (b) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (a)]))$
45	11 44	rspcimedv	$⊢ ((((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \land ⟨1^{st} (u), s⟩ \in (N Sat F) (Y)) \to ((\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)]))$
46	45	ex	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to (⟨1^{st} (u), s⟩ \in (N Sat F) (Y) \to ((\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)])))$
47	46	exlimdv	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to (\exists s ⟨1^{st} (u), s⟩ \in (N Sat F) (Y) \to ((\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)])))$
48	10 47	syl5bi	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to (1^{st} (u) \in dom (N Sat F) (Y) \to ((\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)])))$
49	7 48	sylbid	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to (1^{st} (u) \in dom (M Sat E) (Y) \to ((\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)])))$
50	4 49	mpd	$⊢ (((M \in V \land E \in W \land Y \in ω) \land dom (M Sat E) (Y) = dom (N Sat F) (Y)) \land u \in (M Sat E) (Y)) \to ((\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)]))$
51	50	rexlimdva	$⊢ ((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)]))$

Metamath Proof Explorer

Theorem satfdmlem

Proof