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

Metamath Proof Explorer

Theorem cvrval3

Description: Binary relation expressing Y covers X . (Contributed by NM, 16-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 cvrval3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrval3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrval3.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrval3.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 cvrval3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
7 1 6 4 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
8 1 2 6 3 4 5 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )
9 7 8 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )
10 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) )
11 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝐾 ∈ HL )
12 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
13 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑝 ∈ 𝐴 )
14 1 2 3 4 5 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) → ( ¬ 𝑝 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
15 11 12 13 14 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ( ¬ 𝑝 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
16 10 15 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ¬ 𝑝 ≤ 𝑋 )
17 11 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝐾 ∈ Lat )
18 1 5 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
19 18 3ad2ant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑝 ∈ 𝐵 )
20 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑝 ) ∈ 𝐵 )
21 17 12 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ( 𝑋 ∨ 𝑝 ) ∈ 𝐵 )
22 1 6 4 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑝 ) ∈ 𝐵 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑝 ) )
23 11 12 21 10 22 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑝 ) )
24 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 )
25 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
26 11 25 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝐾 ∈ Poset )
27 simp1l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑌 ∈ 𝐵 )
28 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 )
29 1 2 6 4 cvrnbtwn2 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑝 ) ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ↔ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
30 26 12 27 21 28 29 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ( ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ↔ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
31 23 24 30 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ( 𝑋 ∨ 𝑝 ) = 𝑌 )
32 16 31 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) → ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
33 32 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑝 ∈ 𝐴 → ( ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) → ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) ) )
34 33 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )
35 9 34 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
36 35 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )
37 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → ¬ 𝑝 ≤ 𝑋 )
38 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → 𝐾 ∈ HL )
39 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → 𝑋 ∈ 𝐵 )
40 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → 𝑝 ∈ 𝐴 )
41 38 39 40 14 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → ( ¬ 𝑝 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
42 37 41 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) )
43 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → ( 𝑋 ∨ 𝑝 ) = 𝑌 )
44 42 43 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) → 𝑋 𝐶 𝑌 )
45 44 rexlimdv3a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝑋 𝐶 𝑌 ) )
46 36 45 impbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )