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

Metamath Proof Explorer

Theorem cvrval5

Description: Binary relation expressing X covers X ./\ Y . (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses cvrval5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrval5.l ⊢ ≤ = ( le ‘ 𝐾 )
cvrval5.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrval5.m ⊢ ∧ = ( meet ‘ 𝐾 )
cvrval5.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
cvrval5.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrval5 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cvrval5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrval5.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrval5.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrval5.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cvrval5.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6 cvrval5.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ HL )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
10 8 9 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
11 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 1 2 3 5 6 cvrval3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ) )
13 7 10 11 12 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ) )
14 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
15 14 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → 𝐾 ∈ Lat )
16 10 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
17 1 6 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
18 17 ad2antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → 𝑝 ∈ 𝐵 )
19 1 2 3 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ≤ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) )
20 15 16 18 19 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → 𝑝 ≤ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) )
21 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 )
22 20 21 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → 𝑝 ≤ 𝑋 )
23 22 biantrurd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → ( 𝑝 ≤ 𝑌 ↔ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
24 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → 𝑋 ∈ 𝐵 )
25 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → 𝑌 ∈ 𝐵 )
26 1 2 4 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ) )
27 15 18 24 25 26 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ) )
28 23 27 bitr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → ( 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ↔ 𝑝 ≤ 𝑌 ) )
29 28 notbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) → ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ↔ ¬ 𝑝 ≤ 𝑌 ) )
30 29 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 → ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ↔ ¬ 𝑝 ≤ 𝑌 ) ) )
31 30 pm5.32rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑌 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ) )
32 14 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ Lat )
33 10 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
34 17 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
35 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) )
36 32 33 34 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) )
37 36 eqeq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ↔ ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) )
38 37 anbi2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ 𝑌 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) ) )
39 31 38 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) ) )
40 39 rexbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑋 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) ) )
41 13 40 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) ) )