Metamath Proof Explorer


Theorem joinle

Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011)

Ref Expression
Hypotheses joinle.b 𝐵 = ( Base ‘ 𝐾 )
joinle.l = ( le ‘ 𝐾 )
joinle.j = ( join ‘ 𝐾 )
joinle.k ( 𝜑𝐾 ∈ Poset )
joinle.x ( 𝜑𝑋𝐵 )
joinle.y ( 𝜑𝑌𝐵 )
joinle.z ( 𝜑𝑍𝐵 )
joinle.e ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom )
Assertion joinle ( 𝜑 → ( ( 𝑋 𝑍𝑌 𝑍 ) ↔ ( 𝑋 𝑌 ) 𝑍 ) )

Proof

Step Hyp Ref Expression
1 joinle.b 𝐵 = ( Base ‘ 𝐾 )
2 joinle.l = ( le ‘ 𝐾 )
3 joinle.j = ( join ‘ 𝐾 )
4 joinle.k ( 𝜑𝐾 ∈ Poset )
5 joinle.x ( 𝜑𝑋𝐵 )
6 joinle.y ( 𝜑𝑌𝐵 )
7 joinle.z ( 𝜑𝑍𝐵 )
8 joinle.e ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom )
9 breq2 ( 𝑧 = 𝑍 → ( 𝑋 𝑧𝑋 𝑍 ) )
10 breq2 ( 𝑧 = 𝑍 → ( 𝑌 𝑧𝑌 𝑍 ) )
11 9 10 anbi12d ( 𝑧 = 𝑍 → ( ( 𝑋 𝑧𝑌 𝑧 ) ↔ ( 𝑋 𝑍𝑌 𝑍 ) ) )
12 breq2 ( 𝑧 = 𝑍 → ( ( 𝑋 𝑌 ) 𝑧 ↔ ( 𝑋 𝑌 ) 𝑍 ) )
13 11 12 imbi12d ( 𝑧 = 𝑍 → ( ( ( 𝑋 𝑧𝑌 𝑧 ) → ( 𝑋 𝑌 ) 𝑧 ) ↔ ( ( 𝑋 𝑍𝑌 𝑍 ) → ( 𝑋 𝑌 ) 𝑍 ) ) )
14 1 2 3 4 5 6 8 joinlem ( 𝜑 → ( ( 𝑋 ( 𝑋 𝑌 ) ∧ 𝑌 ( 𝑋 𝑌 ) ) ∧ ∀ 𝑧𝐵 ( ( 𝑋 𝑧𝑌 𝑧 ) → ( 𝑋 𝑌 ) 𝑧 ) ) )
15 14 simprd ( 𝜑 → ∀ 𝑧𝐵 ( ( 𝑋 𝑧𝑌 𝑧 ) → ( 𝑋 𝑌 ) 𝑧 ) )
16 13 15 7 rspcdva ( 𝜑 → ( ( 𝑋 𝑍𝑌 𝑍 ) → ( 𝑋 𝑌 ) 𝑍 ) )
17 1 2 3 4 5 6 8 lejoin1 ( 𝜑𝑋 ( 𝑋 𝑌 ) )
18 1 3 4 5 6 8 joincl ( 𝜑 → ( 𝑋 𝑌 ) ∈ 𝐵 )
19 1 2 postr ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵 ∧ ( 𝑋 𝑌 ) ∈ 𝐵𝑍𝐵 ) ) → ( ( 𝑋 ( 𝑋 𝑌 ) ∧ ( 𝑋 𝑌 ) 𝑍 ) → 𝑋 𝑍 ) )
20 4 5 18 7 19 syl13anc ( 𝜑 → ( ( 𝑋 ( 𝑋 𝑌 ) ∧ ( 𝑋 𝑌 ) 𝑍 ) → 𝑋 𝑍 ) )
21 17 20 mpand ( 𝜑 → ( ( 𝑋 𝑌 ) 𝑍𝑋 𝑍 ) )
22 1 2 3 4 5 6 8 lejoin2 ( 𝜑𝑌 ( 𝑋 𝑌 ) )
23 1 2 postr ( ( 𝐾 ∈ Poset ∧ ( 𝑌𝐵 ∧ ( 𝑋 𝑌 ) ∈ 𝐵𝑍𝐵 ) ) → ( ( 𝑌 ( 𝑋 𝑌 ) ∧ ( 𝑋 𝑌 ) 𝑍 ) → 𝑌 𝑍 ) )
24 4 6 18 7 23 syl13anc ( 𝜑 → ( ( 𝑌 ( 𝑋 𝑌 ) ∧ ( 𝑋 𝑌 ) 𝑍 ) → 𝑌 𝑍 ) )
25 22 24 mpand ( 𝜑 → ( ( 𝑋 𝑌 ) 𝑍𝑌 𝑍 ) )
26 21 25 jcad ( 𝜑 → ( ( 𝑋 𝑌 ) 𝑍 → ( 𝑋 𝑍𝑌 𝑍 ) ) )
27 16 26 impbid ( 𝜑 → ( ( 𝑋 𝑍𝑌 𝑍 ) ↔ ( 𝑋 𝑌 ) 𝑍 ) )