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 syl5bir ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋𝐵𝑌𝐵 ) → ( ∀ 𝑝𝐴 ( 𝑝 𝑋𝑝 𝑌 ) → 𝑋 𝑌 ) )
32 14 31 impbid ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ↔ ∀ 𝑝𝐴 ( 𝑝 𝑋𝑝 𝑌 ) ) )