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

Metamath Proof Explorer

Theorem atlatle

Description: The ordering of two Hilbert lattice elements is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses atlatle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atlatle.l ⊢ ≤ = ( le ‘ 𝐾 )
atlatle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atlatle ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 atlatle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atlatle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atlatle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl13 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
5 atlpos ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
6 4 5 syl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ Poset )
7 1 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
8 7 adantl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
9 simpl2 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
10 simpl3 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
11 1 2 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑝 ≤ 𝑌 ) )
12 6 8 9 10 11 syl13anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑝 ≤ 𝑌 ) )
13 12 expcomd ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑋 ≤ 𝑌 → ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )
14 13 ralrimdva ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )
15 ss2rab ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) )
16 simpl12 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) → 𝐾 ∈ CLat )
17 ssrab2 ⊢ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ⊆ 𝐴
18 1 3 atssbase ⊢ 𝐴 ⊆ 𝐵
19 17 18 sstri ⊢ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ⊆ 𝐵
20 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
21 1 2 20 lubss ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ⊆ 𝐵 ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) ≤ ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) )
22 19 21 mp3an2 ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) ≤ ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) )
23 16 22 sylancom ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) ≤ ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) )
24 23 ex ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) ≤ ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) ) )
25 1 2 20 3 atlatmstc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) = 𝑋 )
26 25 3adant3 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) = 𝑋 )
27 1 2 20 3 atlatmstc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑌 ∈ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) = 𝑌 )
28 27 3adant2 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) = 𝑌 )
29 26 28 breq12d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ) ≤ ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } ) ↔ 𝑋 ≤ 𝑌 ) )
30 24 29 sylibd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌 } → 𝑋 ≤ 𝑌 ) )
31 15 30 biimtrrid ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) )
32 14 31 impbid ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )