Metamath Proof Explorer

Theorem cvrval4N

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

Ref Expression
Hypotheses cvrval4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrval4.s ⊢ < = ( lt ‘ 𝐾 )
cvrval4.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrval4.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
cvrval4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrval4N ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 cvrval4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrval4.s ⊢ < = ( lt ‘ 𝐾 )
3 cvrval4.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrval4.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 cvrval4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 1 2 4 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 1 7 3 4 5 cvrval3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )
9 simpr ⊢ ( ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ( 𝑋 ∨ 𝑝 ) = 𝑌 )
10 9 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 )
11 8 10 biimtrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
12 11 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 )
13 6 12 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 < 𝑌 ∧ ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
14 13 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → ( 𝑋 < 𝑌 ∧ ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )
15 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝑋 < 𝑌 )
16 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ( 𝑋 ∨ 𝑝 ) = 𝑌 )
17 15 16 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝑋 < ( 𝑋 ∨ 𝑝 ) )
18 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝐾 ∈ HL )
19 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝑋 ∈ 𝐵 )
20 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝑝 ∈ 𝐴 )
21 1 7 3 4 5 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
22 18 19 20 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
23 1 2 3 4 5 cvr2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑋 < ( 𝑋 ∨ 𝑝 ) ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
24 18 19 20 23 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ( 𝑋 < ( 𝑋 ∨ 𝑝 ) ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
25 22 24 bitr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑋 < ( 𝑋 ∨ 𝑝 ) ) )
26 17 25 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 )
27 26 16 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) )
28 27 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑝 ∈ 𝐴 → ( ( 𝑋 ∨ 𝑝 ) = 𝑌 → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) ) )
29 28 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )
30 29 expimpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )
31 30 8 sylibrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) → 𝑋 𝐶 𝑌 ) )
32 14 31 impbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ∃ 𝑝 ∈ 𝐴 ( 𝑋 ∨ 𝑝 ) = 𝑌 ) ) )