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 ) → ( 𝐴 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⋖ ( ⊥ ‘ 𝐴 ) ) )