joinval

Description: Join value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom U requirement. (Contributed by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	joindef.u	$⊢ U = lub (K)$
	joindef.j	$⊢ \underset{˙}{\lor} = join (K)$
	joindef.k	$⊢ φ \to K \in V$
	joindef.x	$⊢ φ \to X \in W$
	joindef.y	$⊢ φ \to Y \in Z$
Assertion	joinval	$⊢ φ \to X \underset{˙}{\lor} Y = U (\{X, Y\})$

Proof

Step	Hyp	Ref	Expression
1		joindef.u	$⊢ U = lub (K)$
2		joindef.j	$⊢ \underset{˙}{\lor} = join (K)$
3		joindef.k	$⊢ φ \to K \in V$
4		joindef.x	$⊢ φ \to X \in W$
5		joindef.y	$⊢ φ \to Y \in Z$
6	1 2	joinfval2	$⊢ K \in V \to \underset{˙}{\lor} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\}$
7	3 6	syl	$⊢ φ \to \underset{˙}{\lor} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\}$
8	7	oveqd	$⊢ φ \to X \underset{˙}{\lor} Y = X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} Y$
9	8	adantr	$⊢ (φ \land \{X, Y\} \in dom U) \to X \underset{˙}{\lor} Y = X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} Y$
10		simpr	$⊢ (φ \land \{X, Y\} \in dom U) \to \{X, Y\} \in dom U$
11		eqidd	$⊢ (φ \land \{X, Y\} \in dom U) \to U (\{X, Y\}) = U (\{X, Y\})$
12		fvexd	$⊢ φ \to U (\{X, Y\}) \in V$
13		preq12	$⊢ (x = X \land y = Y) \to \{x, y\} = \{X, Y\}$
14	13	eleq1d	$⊢ (x = X \land y = Y) \to (\{x, y\} \in dom U \leftrightarrow \{X, Y\} \in dom U)$
15	14	3adant3	$⊢ (x = X \land y = Y \land z = U (\{X, Y\})) \to (\{x, y\} \in dom U \leftrightarrow \{X, Y\} \in dom U)$
16		simp3	$⊢ (x = X \land y = Y \land z = U (\{X, Y\})) \to z = U (\{X, Y\})$
17	13	fveq2d	$⊢ (x = X \land y = Y) \to U (\{x, y\}) = U (\{X, Y\})$
18	17	3adant3	$⊢ (x = X \land y = Y \land z = U (\{X, Y\})) \to U (\{x, y\}) = U (\{X, Y\})$
19	16 18	eqeq12d	$⊢ (x = X \land y = Y \land z = U (\{X, Y\})) \to (z = U (\{x, y\}) \leftrightarrow U (\{X, Y\}) = U (\{X, Y\}))$
20	15 19	anbi12d	$⊢ (x = X \land y = Y \land z = U (\{X, Y\})) \to ((\{x, y\} \in dom U \land z = U (\{x, y\})) \leftrightarrow (\{X, Y\} \in dom U \land U (\{X, Y\}) = U (\{X, Y\})))$
21		moeq	$⊢ \exists^{*} z z = U (\{x, y\})$
22	21	moani	$⊢ \exists^{*} z (\{x, y\} \in dom U \land z = U (\{x, y\}))$
23		eqid	$⊢ \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\}$
24	20 22 23	ovigg	$⊢ (X \in W \land Y \in Z \land U (\{X, Y\}) \in V) \to ((\{X, Y\} \in dom U \land U (\{X, Y\}) = U (\{X, Y\})) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} Y = U (\{X, Y\}))$
25	4 5 12 24	syl3anc	$⊢ φ \to ((\{X, Y\} \in dom U \land U (\{X, Y\}) = U (\{X, Y\})) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} Y = U (\{X, Y\}))$
26	25	adantr	$⊢ (φ \land \{X, Y\} \in dom U) \to ((\{X, Y\} \in dom U \land U (\{X, Y\}) = U (\{X, Y\})) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} Y = U (\{X, Y\}))$
27	10 11 26	mp2and	$⊢ (φ \land \{X, Y\} \in dom U) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} Y = U (\{X, Y\})$
28	9 27	eqtrd	$⊢ (φ \land \{X, Y\} \in dom U) \to X \underset{˙}{\lor} Y = U (\{X, Y\})$
29	1 2 3 4 5	joindef	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \leftrightarrow \{X, Y\} \in dom U)$
30	29	notbid	$⊢ φ \to (\neg ⟨X, Y⟩ \in dom \underset{˙}{\lor} \leftrightarrow \neg \{X, Y\} \in dom U)$
31		df-ov	$⊢ X \underset{˙}{\lor} Y = \underset{˙}{\lor} (⟨X, Y⟩)$
32		ndmfv	$⊢ \neg ⟨X, Y⟩ \in dom \underset{˙}{\lor} \to \underset{˙}{\lor} (⟨X, Y⟩) = \emptyset$
33	31 32	syl5eq	$⊢ \neg ⟨X, Y⟩ \in dom \underset{˙}{\lor} \to X \underset{˙}{\lor} Y = \emptyset$
34	30 33	syl6bir	$⊢ φ \to (\neg \{X, Y\} \in dom U \to X \underset{˙}{\lor} Y = \emptyset)$
35	34	imp	$⊢ (φ \land \neg \{X, Y\} \in dom U) \to X \underset{˙}{\lor} Y = \emptyset$
36		ndmfv	$⊢ \neg \{X, Y\} \in dom U \to U (\{X, Y\}) = \emptyset$
37	36	adantl	$⊢ (φ \land \neg \{X, Y\} \in dom U) \to U (\{X, Y\}) = \emptyset$
38	35 37	eqtr4d	$⊢ (φ \land \neg \{X, Y\} \in dom U) \to X \underset{˙}{\lor} Y = U (\{X, Y\})$
39	28 38	pm2.61dan	$⊢ φ \to X \underset{˙}{\lor} Y = U (\{X, Y\})$

Metamath Proof Explorer

Theorem joinval

Proof