joindm3

Description: The join of any two elements always exists iff all unordered pairs have LUB (expanded version). (Contributed by Zhi Wang, 25-Sep-2024)

	Ref	Expression
Hypotheses	joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	joindm2.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	joindm2.j	⊢ ∨ = ( join ‘ 𝐾 )
	joindm3.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	joindm3	⊢ ( 𝜑 → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 ∈ 𝐵 ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
3		joindm2.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
4		joindm2.j	⊢ ∨ = ( join ‘ 𝐾 )
5		joindm3.l	⊢ ≤ = ( le ‘ 𝐾 )
6	1 2 3 4	joindm2	⊢ ( 𝜑 → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝑈 ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
9	7 8	prssd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → { 𝑥 , 𝑦 } ⊆ 𝐵 )
10		biid	⊢ ( ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ↔ ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) )
11	1 5 3 10 2	lubeldm	⊢ ( 𝜑 → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ) ) )
12	11	baibd	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ⊆ 𝐵 ) → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ) )
13	9 12	syldan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ) )
14	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ 𝑉 )
15	1 5 4 14 7 8	joinval2lem	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ↔ ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )
16	15	reubidv	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ↔ ∃! 𝑧 ∈ 𝐵 ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑣 ≤ 𝑤 → 𝑧 ≤ 𝑤 ) ) ↔ ∃! 𝑧 ∈ 𝐵 ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )
18	13 17	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ ∃! 𝑧 ∈ 𝐵 ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )
19	18	2ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 ∈ 𝐵 ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )
20	6 19	bitrd	⊢ ( 𝜑 → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 ∈ 𝐵 ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤 ) → 𝑧 ≤ 𝑤 ) ) ) )

Metamath Proof Explorer

Theorem joindm3

Proof