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 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 ◡ < 𝑑 ) ) ) )