joinfval

Description: Value of join function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018) TODO: prove joinfval2 first to reduce net proof size (existence part)?

	Ref	Expression
Hypotheses	joinfval.u	$⊢ U = lub (K)$
	joinfval.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	joinfval	$⊢ K \in V \to \underset{˙}{\lor} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\}$

Proof

Step	Hyp	Ref	Expression
1		joinfval.u	$⊢ U = lub (K)$
2		joinfval.j	$⊢ \underset{˙}{\lor} = join (K)$
3		elex	$⊢ K \in V \to K \in V$
4		fvex	$⊢ {Base}_{K} \in V$
5		moeq	$⊢ \exists^{*} z z = U (\{x, y\})$
6	5	a1i	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \to \exists^{*} z z = U (\{x, y\})$
7		eqid	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))\}$
8	4 4 6 7	oprabex	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))\} \in V$
9	8	a1i	$⊢ K \in V \to \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))\} \in V$
10	1	lubfun	$⊢ Fun U$
11		funbrfv2b	$⊢ Fun U \to (\{x, y\} U z \leftrightarrow (\{x, y\} \in dom U \land U (\{x, y\}) = z))$
12	10 11	ax-mp	$⊢ \{x, y\} U z \leftrightarrow (\{x, y\} \in dom U \land U (\{x, y\}) = z)$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15		simpl	$⊢ (K \in V \land \{x, y\} \in dom U) \to K \in V$
16		simpr	$⊢ (K \in V \land \{x, y\} \in dom U) \to \{x, y\} \in dom U$
17	13 14 1 15 16	lubelss	$⊢ (K \in V \land \{x, y\} \in dom U) \to \{x, y\} \subseteq {Base}_{K}$
18	17	ex	$⊢ K \in V \to (\{x, y\} \in dom U \to \{x, y\} \subseteq {Base}_{K})$
19		vex	$⊢ x \in V$
20		vex	$⊢ y \in V$
21	19 20	prss	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \leftrightarrow \{x, y\} \subseteq {Base}_{K}$
22	18 21	imbitrrdi	$⊢ K \in V \to (\{x, y\} \in dom U \to (x \in {Base}_{K} \land y \in {Base}_{K}))$
23		eqcom	$⊢ U (\{x, y\}) = z \leftrightarrow z = U (\{x, y\})$
24	23	biimpi	$⊢ U (\{x, y\}) = z \to z = U (\{x, y\})$
25	22 24	anim12d1	$⊢ K \in V \to ((\{x, y\} \in dom U \land U (\{x, y\}) = z) \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\})))$
26	12 25	biimtrid	$⊢ K \in V \to (\{x, y\} U z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\})))$
27	26	alrimiv	$⊢ K \in V \to \forall z (\{x, y\} U z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\})))$
28	27	alrimiv	$⊢ K \in V \to \forall y \forall z (\{x, y\} U z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\})))$
29	28	alrimiv	$⊢ K \in V \to \forall x \forall y \forall z (\{x, y\} U z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\})))$
30		ssoprab2	$⊢ \forall x \forall y \forall z (\{x, y\} U z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))) \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))\}$
31	29 30	syl	$⊢ K \in V \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = U (\{x, y\}))\}$
32	9 31	ssexd	$⊢ K \in V \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\} \in V$
33		fveq2	$⊢ p = K \to lub (p) = lub (K)$
34	33 1	eqtr4di	$⊢ p = K \to lub (p) = U$
35	34	breqd	$⊢ p = K \to (\{x, y\} lub (p) z \leftrightarrow \{x, y\} U z)$
36	35	oprabbidv	$⊢ p = K \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} lub (p) z\} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\}$
37		df-join	$⊢ join = (p \in V ⟼ \{⟨⟨x, y⟩, z⟩ \| \{x, y\} lub (p) z\})$
38	36 37	fvmptg	$⊢ (K \in V \land \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\} \in V) \to join (K) = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\}$
39	32 38	mpdan	$⊢ K \in V \to join (K) = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\}$
40	2 39	eqtrid	$⊢ K \in V \to \underset{˙}{\lor} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\}$
41	3 40	syl	$⊢ K \in V \to \underset{˙}{\lor} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} U z\}$

Metamath Proof Explorer

Theorem joinfval

Proof