This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihord6b

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihord3.l ⊢ ≤ = ( le ‘ 𝐾 )
dihord3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihord3.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihord6b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dihord3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihord3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihord3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihord3.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ¬ 𝑋 ≤ 𝑊 )
6 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ≤ 𝑊 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
9 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
10 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ 𝐵 )
11 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
12 1 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
13 11 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
14 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑊 ) → 𝑋 ≤ 𝑊 ) )
15 8 9 10 13 14 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑊 ) → 𝑋 ≤ 𝑊 ) )
16 6 15 mpan2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 → 𝑋 ≤ 𝑊 ) )
17 5 16 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ¬ 𝑋 ≤ 𝑌 )
18 17 pm2.21d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) )
19 18 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) )