Metamath Proof Explorer


Theorem tosglblem

Description: Lemma for tosglb and xrsclat . (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by NM, 15-Sep-2018)

Ref Expression
Hypotheses tosglb.b 𝐵 = ( Base ‘ 𝐾 )
tosglb.l < = ( lt ‘ 𝐾 )
tosglb.1 ( 𝜑𝐾 ∈ Toset )
tosglb.2 ( 𝜑𝐴𝐵 )
tosglb.e = ( le ‘ 𝐾 )
Assertion tosglblem ( ( 𝜑𝑎𝐵 ) → ( ( ∀ 𝑏𝐴 𝑎 𝑏 ∧ ∀ 𝑐𝐵 ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ) ↔ ( ∀ 𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑𝐴 𝑏 < 𝑑 ) ) ) )

Proof

Step Hyp Ref Expression
1 tosglb.b 𝐵 = ( Base ‘ 𝐾 )
2 tosglb.l < = ( lt ‘ 𝐾 )
3 tosglb.1 ( 𝜑𝐾 ∈ Toset )
4 tosglb.2 ( 𝜑𝐴𝐵 )
5 tosglb.e = ( le ‘ 𝐾 )
6 3 ad2antrr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑏𝐴 ) → 𝐾 ∈ Toset )
7 4 adantr ( ( 𝜑𝑎𝐵 ) → 𝐴𝐵 )
8 7 sselda ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑏𝐴 ) → 𝑏𝐵 )
9 simplr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑏𝐴 ) → 𝑎𝐵 )
10 1 5 2 tltnle ( ( 𝐾 ∈ Toset ∧ 𝑏𝐵𝑎𝐵 ) → ( 𝑏 < 𝑎 ↔ ¬ 𝑎 𝑏 ) )
11 6 8 9 10 syl3anc ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑏𝐴 ) → ( 𝑏 < 𝑎 ↔ ¬ 𝑎 𝑏 ) )
12 11 con2bid ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑏𝐴 ) → ( 𝑎 𝑏 ↔ ¬ 𝑏 < 𝑎 ) )
13 12 ralbidva ( ( 𝜑𝑎𝐵 ) → ( ∀ 𝑏𝐴 𝑎 𝑏 ↔ ∀ 𝑏𝐴 ¬ 𝑏 < 𝑎 ) )
14 4 ad2antrr ( ( ( 𝜑𝑐𝐵 ) ∧ 𝑏𝐴 ) → 𝐴𝐵 )
15 simpr ( ( ( 𝜑𝑐𝐵 ) ∧ 𝑏𝐴 ) → 𝑏𝐴 )
16 14 15 sseldd ( ( ( 𝜑𝑐𝐵 ) ∧ 𝑏𝐴 ) → 𝑏𝐵 )
17 1 5 2 tltnle ( ( 𝐾 ∈ Toset ∧ 𝑏𝐵𝑐𝐵 ) → ( 𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏 ) )
18 3 17 syl3an1 ( ( 𝜑𝑏𝐵𝑐𝐵 ) → ( 𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏 ) )
19 18 3com23 ( ( 𝜑𝑐𝐵𝑏𝐵 ) → ( 𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏 ) )
20 19 3expa ( ( ( 𝜑𝑐𝐵 ) ∧ 𝑏𝐵 ) → ( 𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏 ) )
21 20 con2bid ( ( ( 𝜑𝑐𝐵 ) ∧ 𝑏𝐵 ) → ( 𝑐 𝑏 ↔ ¬ 𝑏 < 𝑐 ) )
22 16 21 syldan ( ( ( 𝜑𝑐𝐵 ) ∧ 𝑏𝐴 ) → ( 𝑐 𝑏 ↔ ¬ 𝑏 < 𝑐 ) )
23 22 ralbidva ( ( 𝜑𝑐𝐵 ) → ( ∀ 𝑏𝐴 𝑐 𝑏 ↔ ∀ 𝑏𝐴 ¬ 𝑏 < 𝑐 ) )
24 breq1 ( 𝑏 = 𝑑 → ( 𝑏 < 𝑐𝑑 < 𝑐 ) )
25 24 notbid ( 𝑏 = 𝑑 → ( ¬ 𝑏 < 𝑐 ↔ ¬ 𝑑 < 𝑐 ) )
26 25 cbvralvw ( ∀ 𝑏𝐴 ¬ 𝑏 < 𝑐 ↔ ∀ 𝑑𝐴 ¬ 𝑑 < 𝑐 )
27 ralnex ( ∀ 𝑑𝐴 ¬ 𝑑 < 𝑐 ↔ ¬ ∃ 𝑑𝐴 𝑑 < 𝑐 )
28 26 27 bitri ( ∀ 𝑏𝐴 ¬ 𝑏 < 𝑐 ↔ ¬ ∃ 𝑑𝐴 𝑑 < 𝑐 )
29 23 28 bitrdi ( ( 𝜑𝑐𝐵 ) → ( ∀ 𝑏𝐴 𝑐 𝑏 ↔ ¬ ∃ 𝑑𝐴 𝑑 < 𝑐 ) )
30 29 adantlr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → ( ∀ 𝑏𝐴 𝑐 𝑏 ↔ ¬ ∃ 𝑑𝐴 𝑑 < 𝑐 ) )
31 3 ad2antrr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → 𝐾 ∈ Toset )
32 simplr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → 𝑎𝐵 )
33 simpr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → 𝑐𝐵 )
34 1 5 2 tltnle ( ( 𝐾 ∈ Toset ∧ 𝑎𝐵𝑐𝐵 ) → ( 𝑎 < 𝑐 ↔ ¬ 𝑐 𝑎 ) )
35 31 32 33 34 syl3anc ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → ( 𝑎 < 𝑐 ↔ ¬ 𝑐 𝑎 ) )
36 35 con2bid ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → ( 𝑐 𝑎 ↔ ¬ 𝑎 < 𝑐 ) )
37 30 36 imbi12d ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → ( ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ↔ ( ¬ ∃ 𝑑𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐 ) ) )
38 con34b ( ( 𝑎 < 𝑐 → ∃ 𝑑𝐴 𝑑 < 𝑐 ) ↔ ( ¬ ∃ 𝑑𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐 ) )
39 37 38 bitr4di ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑐𝐵 ) → ( ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ↔ ( 𝑎 < 𝑐 → ∃ 𝑑𝐴 𝑑 < 𝑐 ) ) )
40 39 ralbidva ( ( 𝜑𝑎𝐵 ) → ( ∀ 𝑐𝐵 ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ↔ ∀ 𝑐𝐵 ( 𝑎 < 𝑐 → ∃ 𝑑𝐴 𝑑 < 𝑐 ) ) )
41 breq2 ( 𝑏 = 𝑐 → ( 𝑎 < 𝑏𝑎 < 𝑐 ) )
42 breq2 ( 𝑏 = 𝑐 → ( 𝑑 < 𝑏𝑑 < 𝑐 ) )
43 42 rexbidv ( 𝑏 = 𝑐 → ( ∃ 𝑑𝐴 𝑑 < 𝑏 ↔ ∃ 𝑑𝐴 𝑑 < 𝑐 ) )
44 41 43 imbi12d ( 𝑏 = 𝑐 → ( ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) ↔ ( 𝑎 < 𝑐 → ∃ 𝑑𝐴 𝑑 < 𝑐 ) ) )
45 44 cbvralvw ( ∀ 𝑏𝐵 ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) ↔ ∀ 𝑐𝐵 ( 𝑎 < 𝑐 → ∃ 𝑑𝐴 𝑑 < 𝑐 ) )
46 40 45 bitr4di ( ( 𝜑𝑎𝐵 ) → ( ∀ 𝑐𝐵 ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ↔ ∀ 𝑏𝐵 ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) ) )
47 13 46 anbi12d ( ( 𝜑𝑎𝐵 ) → ( ( ∀ 𝑏𝐴 𝑎 𝑏 ∧ ∀ 𝑐𝐵 ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ) ↔ ( ∀ 𝑏𝐴 ¬ 𝑏 < 𝑎 ∧ ∀ 𝑏𝐵 ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) ) ) )
48 vex 𝑎 ∈ V
49 vex 𝑏 ∈ V
50 48 49 brcnv ( 𝑎 < 𝑏𝑏 < 𝑎 )
51 50 notbii ( ¬ 𝑎 < 𝑏 ↔ ¬ 𝑏 < 𝑎 )
52 51 ralbii ( ∀ 𝑏𝐴 ¬ 𝑎 < 𝑏 ↔ ∀ 𝑏𝐴 ¬ 𝑏 < 𝑎 )
53 49 48 brcnv ( 𝑏 < 𝑎𝑎 < 𝑏 )
54 vex 𝑑 ∈ V
55 49 54 brcnv ( 𝑏 < 𝑑𝑑 < 𝑏 )
56 55 rexbii ( ∃ 𝑑𝐴 𝑏 < 𝑑 ↔ ∃ 𝑑𝐴 𝑑 < 𝑏 )
57 53 56 imbi12i ( ( 𝑏 < 𝑎 → ∃ 𝑑𝐴 𝑏 < 𝑑 ) ↔ ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) )
58 57 ralbii ( ∀ 𝑏𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑𝐴 𝑏 < 𝑑 ) ↔ ∀ 𝑏𝐵 ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) )
59 52 58 anbi12i ( ( ∀ 𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑𝐴 𝑏 < 𝑑 ) ) ↔ ( ∀ 𝑏𝐴 ¬ 𝑏 < 𝑎 ∧ ∀ 𝑏𝐵 ( 𝑎 < 𝑏 → ∃ 𝑑𝐴 𝑑 < 𝑏 ) ) )
60 47 59 bitr4di ( ( 𝜑𝑎𝐵 ) → ( ( ∀ 𝑏𝐴 𝑎 𝑏 ∧ ∀ 𝑐𝐵 ( ∀ 𝑏𝐴 𝑐 𝑏𝑐 𝑎 ) ) ↔ ( ∀ 𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑𝐴 𝑏 < 𝑑 ) ) ) )