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

Metamath Proof Explorer

Theorem atlrelat1

Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)

Ref Expression
Hypotheses atlrelat1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atlrelat1.l ⊢ ≤ = ( le ‘ 𝐾 )
atlrelat1.s ⊢ < = ( lt ‘ 𝐾 )
atlrelat1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atlrelat1 ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 atlrelat1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atlrelat1.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atlrelat1.s ⊢ < = ( lt ‘ 𝐾 )
4 atlrelat1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simp13 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
6 atlpos ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
7 5 6 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Poset )
8 1 2 3 pltnle ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ¬ 𝑌 ≤ 𝑋 )
9 8 ex ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ¬ 𝑌 ≤ 𝑋 ) )
10 7 9 syld3an1 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ¬ 𝑌 ≤ 𝑋 ) )
11 iman ⊢ ( ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ↔ ¬ ( 𝑝 ≤ 𝑌 ∧ ¬ 𝑝 ≤ 𝑋 ) )
12 ancom ⊢ ( ( 𝑝 ≤ 𝑌 ∧ ¬ 𝑝 ≤ 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) )
13 11 12 xchbinx ⊢ ( ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ↔ ¬ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) )
14 13 ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ¬ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) )
15 1 2 4 atlatle ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ) )
16 15 3com23 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ) )
17 16 biimprd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) → 𝑌 ≤ 𝑋 ) )
18 14 17 biimtrrid ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ¬ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) → 𝑌 ≤ 𝑋 ) )
19 18 con3d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑌 ≤ 𝑋 → ¬ ∀ 𝑝 ∈ 𝐴 ¬ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
20 dfrex2 ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ ¬ ∀ 𝑝 ∈ 𝐴 ¬ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) )
21 19 20 imbitrrdi ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑌 ≤ 𝑋 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
22 10 21 syld ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )