joindmss

Description: Subset property of domain of join. (Contributed by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	joindmss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joindmss.j	⊢ ∨ = ( join ‘ 𝐾 )
	joindmss.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion	joindmss	⊢ ( 𝜑 → dom ∨ ⊆ ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		joindmss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joindmss.j	⊢ ∨ = ( join ‘ 𝐾 )
3		joindmss.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		relopabv	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) }
5		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
6	5 2	joindm	⊢ ( 𝐾 ∈ 𝑉 → dom ∨ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) } )
7	3 6	syl	⊢ ( 𝜑 → dom ∨ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) } )
8	7	releqd	⊢ ( 𝜑 → ( Rel dom ∨ ↔ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) } ) )
9	4 8	mpbiri	⊢ ( 𝜑 → Rel dom ∨ )
10		vex	⊢ 𝑥 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝑥 ∈ V )
12		vex	⊢ 𝑦 ∈ V
13	12	a1i	⊢ ( 𝜑 → 𝑦 ∈ V )
14	5 2 3 11 13	joindef	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ ↔ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) )
15		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
16	3	adantr	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) → 𝐾 ∈ 𝑉 )
17		simpr	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) )
18	1 15 5 16 17	lubelss	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ⊆ 𝐵 )
19	18	ex	⊢ ( 𝜑 → ( { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) → { 𝑥 , 𝑦 } ⊆ 𝐵 ) )
20	10 12	prss	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
21		opelxpi	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
22	20 21	sylbir	⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
23	19 22	syl6	⊢ ( 𝜑 → ( { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ) )
24	14 23	sylbid	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∨ → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ) )
25	9 24	relssdv	⊢ ( 𝜑 → dom ∨ ⊆ ( 𝐵 × 𝐵 ) )

Metamath Proof Explorer

Theorem joindmss

Proof