joindm2

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

	Ref	Expression
Hypotheses	joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	joindm2.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	joindm2.j	⊢ ∨ = ( join ‘ 𝐾 )
Assertion	joindm2	⊢ ( 𝜑 → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
3		joindm2.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
4		joindm2.j	⊢ ∨ = ( join ‘ 𝐾 )
5	1 4 2	joindmss	⊢ ( 𝜑 → dom ∨ ⊆ ( 𝐵 × 𝐵 ) )
6		eqss	⊢ ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ( dom ∨ ⊆ ( 𝐵 × 𝐵 ) ∧ ( 𝐵 × 𝐵 ) ⊆ dom ∨ ) )
7	6	baib	⊢ ( dom ∨ ⊆ ( 𝐵 × 𝐵 ) → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ( 𝐵 × 𝐵 ) ⊆ dom ∨ ) )
8	5 7	syl	⊢ ( 𝜑 → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ( 𝐵 × 𝐵 ) ⊆ dom ∨ ) )
9		relxp	⊢ Rel ( 𝐵 × 𝐵 )
10		ssrel	⊢ ( Rel ( 𝐵 × 𝐵 ) → ( ( 𝐵 × 𝐵 ) ⊆ dom ∨ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ) ) )
11	9 10	mp1i	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) ⊆ dom ∨ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ) ) )
12		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
13	12	a1i	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
14		vex	⊢ 𝑥 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝑥 ∈ V )
16		vex	⊢ 𝑦 ∈ V
17	16	a1i	⊢ ( 𝜑 → 𝑦 ∈ V )
18	3 4 2 15 17	joindef	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ↔ { 𝑥 , 𝑦 } ∈ dom 𝑈 ) )
19	13 18	imbi12d	⊢ ( 𝜑 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ dom 𝑈 ) ) )
20	19	2albidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ dom 𝑈 ) ) )
21		r2al	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ dom 𝑈 ) )
22	20 21	bitr4di	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝑈 ) )
23	8 11 22	3bitrd	⊢ ( 𝜑 → ( dom ∨ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝑈 ) )

Metamath Proof Explorer

Theorem joindm2

Proof