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 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )