satffunlem

		Ref	Expression
	Assertion	satffunlem	$⊢ ((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to y = w$

Proof

Step	Hyp	Ref	Expression
1		eqtr2	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r)) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r)$
2		fvex	$⊢ 1^{st} (u) \in V$
3		fvex	$⊢ 1^{st} (v) \in V$
4		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)⟩⟩$
5	2 3 4	mp2an	$⊢ 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
6		fvex	$⊢ 1^{st} (s) \in V$
7		fvex	$⊢ 1^{st} (r) \in V$
8		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)⟩⟩$
9	6 7 8	mp2an	$⊢ 1^{st} (s) ⊼_{𝑔} 1^{st} (r) = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
10	5 9	eqeq12i	$⊢ 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \leftrightarrow ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩$
11		1oex	$⊢ 1_{𝑜} \in V$
12		opex	$⊢ ⟨1^{st} (u), 1^{st} (v)⟩ \in V$
13	11 12	opth	$⊢ ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ = ⟨1_{𝑜}, ⟨1^{st} (s), 1^{st} (r)⟩⟩ \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨1^{st} (u), 1^{st} (v)⟩ = ⟨1^{st} (s), 1^{st} (r)⟩)$
14	2 3	opth	$⊢ ⟨1^{st} (u), 1^{st} (v)⟩ = ⟨1^{st} (s), 1^{st} (r)⟩ \leftrightarrow (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))$
15	14	anbi2i	$⊢ (1_{𝑜} = 1_{𝑜} \land ⟨1^{st} (u), 1^{st} (v)⟩ = ⟨1^{st} (s), 1^{st} (r)⟩) \leftrightarrow (1_{𝑜} = 1_{𝑜} \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)))$
16	10 13 15	3bitri	$⊢ 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \leftrightarrow (1_{𝑜} = 1_{𝑜} \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)))$
17		funfv1st2nd	$⊢ (Fun Z \land s \in Z) \to Z (1^{st} (s)) = 2^{nd} (s)$
18	17	ex	$⊢ Fun Z \to (s \in Z \to Z (1^{st} (s)) = 2^{nd} (s))$
19		funfv1st2nd	$⊢ (Fun Z \land r \in Z) \to Z (1^{st} (r)) = 2^{nd} (r)$
20	19	ex	$⊢ Fun Z \to (r \in Z \to Z (1^{st} (r)) = 2^{nd} (r))$
21	18 20	anim12d	$⊢ Fun Z \to ((s \in Z \land r \in Z) \to (Z (1^{st} (s)) = 2^{nd} (s) \land Z (1^{st} (r)) = 2^{nd} (r)))$
22		funfv1st2nd	$⊢ (Fun Z \land u \in Z) \to Z (1^{st} (u)) = 2^{nd} (u)$
23	22	ex	$⊢ Fun Z \to (u \in Z \to Z (1^{st} (u)) = 2^{nd} (u))$
24		funfv1st2nd	$⊢ (Fun Z \land v \in Z) \to Z (1^{st} (v)) = 2^{nd} (v)$
25	24	ex	$⊢ Fun Z \to (v \in Z \to Z (1^{st} (v)) = 2^{nd} (v))$
26	23 25	anim12d	$⊢ Fun Z \to ((u \in Z \land v \in Z) \to (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v)))$
27		fveq2	$⊢ 1^{st} (s) = 1^{st} (u) \to Z (1^{st} (s)) = Z (1^{st} (u))$
28	27	eqcoms	$⊢ 1^{st} (u) = 1^{st} (s) \to Z (1^{st} (s)) = Z (1^{st} (u))$
29	28	adantr	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to Z (1^{st} (s)) = Z (1^{st} (u))$
30	29	eqeq1d	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to (Z (1^{st} (s)) = 2^{nd} (s) \leftrightarrow Z (1^{st} (u)) = 2^{nd} (s))$
31		fveq2	$⊢ 1^{st} (r) = 1^{st} (v) \to Z (1^{st} (r)) = Z (1^{st} (v))$
32	31	eqcoms	$⊢ 1^{st} (v) = 1^{st} (r) \to Z (1^{st} (r)) = Z (1^{st} (v))$
33	32	adantl	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to Z (1^{st} (r)) = Z (1^{st} (v))$
34	33	eqeq1d	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to (Z (1^{st} (r)) = 2^{nd} (r) \leftrightarrow Z (1^{st} (v)) = 2^{nd} (r))$
35	30 34	anbi12d	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to ((Z (1^{st} (s)) = 2^{nd} (s) \land Z (1^{st} (r)) = 2^{nd} (r)) \leftrightarrow (Z (1^{st} (u)) = 2^{nd} (s) \land Z (1^{st} (v)) = 2^{nd} (r)))$
36	35	anbi1d	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to (((Z (1^{st} (s)) = 2^{nd} (s) \land Z (1^{st} (r)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \leftrightarrow ((Z (1^{st} (u)) = 2^{nd} (s) \land Z (1^{st} (v)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))))$
37		eqtr2	$⊢ (Z (1^{st} (u)) = 2^{nd} (s) \land Z (1^{st} (u)) = 2^{nd} (u)) \to 2^{nd} (s) = 2^{nd} (u)$
38	37	ad2ant2r	$⊢ ((Z (1^{st} (u)) = 2^{nd} (s) \land Z (1^{st} (v)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \to 2^{nd} (s) = 2^{nd} (u)$
39		eqtr2	$⊢ (Z (1^{st} (v)) = 2^{nd} (r) \land Z (1^{st} (v)) = 2^{nd} (v)) \to 2^{nd} (r) = 2^{nd} (v)$
40	39	ad2ant2l	$⊢ ((Z (1^{st} (u)) = 2^{nd} (s) \land Z (1^{st} (v)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \to 2^{nd} (r) = 2^{nd} (v)$
41	38 40	ineq12d	$⊢ ((Z (1^{st} (u)) = 2^{nd} (s) \land Z (1^{st} (v)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v)$
42	36 41	syl6bi	$⊢ (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to (((Z (1^{st} (s)) = 2^{nd} (s) \land Z (1^{st} (r)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v))$
43	42	com12	$⊢ ((Z (1^{st} (s)) = 2^{nd} (s) \land Z (1^{st} (r)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \to ((1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v))$
44	43	a1i	$⊢ Fun Z \to (((Z (1^{st} (s)) = 2^{nd} (s) \land Z (1^{st} (r)) = 2^{nd} (r)) \land (Z (1^{st} (u)) = 2^{nd} (u) \land Z (1^{st} (v)) = 2^{nd} (v))) \to ((1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v)))$
45	21 26 44	syl2and	$⊢ Fun Z \to (((s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to ((1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v)))$
46	45	expd	$⊢ Fun Z \to ((s \in Z \land r \in Z) \to ((u \in Z \land v \in Z) \to ((1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v))))$
47	46	3imp1	$⊢ ((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))) \to 2^{nd} (s) \cap 2^{nd} (r) = 2^{nd} (u) \cap 2^{nd} (v)$
48	47	difeq2d	$⊢ ((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))) \to (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
49	48	adantr	$⊢ (((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))) \land (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
50		eqeq12	$⊢ (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to (y = w \leftrightarrow (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
51	50	adantl	$⊢ (((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))) \land (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to (y = w \leftrightarrow (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
52	49 51	mpbird	$⊢ (((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))) \land (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to y = w$
53	52	exp43	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to ((1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r)) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to y = w)))$
54	53	adantld	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to ((1_{𝑜} = 1_{𝑜} \land (1^{st} (u) = 1^{st} (s) \land 1^{st} (v) = 1^{st} (r))) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to y = w)))$
55	16 54	syl5bi	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to (1^{st} (u) ⊼_{𝑔} 1^{st} (v) = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to y = w)))$
56	1 55	syl5	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r)) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to y = w)))$
57	56	expd	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to y = w))))$
58	57	com35	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to y = w))))$
59	58	impd	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to y = w)))$
60	59	com24	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \to (y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r)) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to y = w)))$
61	60	impd	$⊢ (Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \to ((x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to y = w))$
62	61	3imp	$⊢ ((Fun Z \land (s \in Z \land r \in Z) \land (u \in Z \land v \in Z)) \land (x = 1^{st} (s) ⊼_{𝑔} 1^{st} (r) \land y = (M^{ω}) ∖ (2^{nd} (s) \cap 2^{nd} (r))) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land w = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to y = w$

Metamath Proof Explorer

Theorem satffunlem

Proof