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

Metamath Proof Explorer

Theorem cvcon3

Description: Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvcon3 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 chpsscon3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
2 chpsscon3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ⊊ 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
3 2 adantlr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ⊊ 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
4 chpsscon3 ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
5 4 ancoms ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
6 5 adantll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
7 3 6 anbi12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ( ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) ) )
8 choccl ⊢ ( 𝑥 ∈ Cℋ → ( ⊥ ‘ 𝑥 ) ∈ Cℋ )
9 psseq2 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
10 psseq1 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
11 9 10 anbi12d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
12 11 rspcev ⊢ ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) )
13 8 12 sylan ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) )
14 13 ex ⊢ ( 𝑥 ∈ Cℋ → ( ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
15 14 ancomsd ⊢ ( 𝑥 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
16 15 adantl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
17 7 16 sylbid ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
18 17 rexlimdva ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
19 chpsscon1 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ↔ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) )
20 19 adantll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ↔ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) )
21 chpsscon2 ⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
22 21 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
23 22 adantlr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
24 20 23 anbi12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ∧ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) ) )
25 choccl ⊢ ( 𝑦 ∈ Cℋ → ( ⊥ ‘ 𝑦 ) ∈ Cℋ )
26 psseq2 ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝐴 ⊊ 𝑥 ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
27 psseq1 ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) )
28 26 27 anbi12d ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) ) )
29 28 rspcev ⊢ ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ ∧ ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) )
30 25 29 sylan ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) )
31 30 ex ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
32 31 ancomsd ⊢ ( 𝑦 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ∧ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
33 32 adantl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ∧ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
34 24 33 sylbid ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
35 34 rexlimdva ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
36 18 35 impbid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
37 36 notbid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
38 1 37 anbi12d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) ) )
39 cvbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) )
40 choccl ⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ 𝐵 ) ∈ Cℋ )
41 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
42 cvbr ⊢ ( ( ( ⊥ ‘ 𝐵 ) ∈ Cℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) ) )
43 40 41 42 syl2anr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) ) )
44 38 39 43 3bitr4d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ) )