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 ⊢ B = Base K
tosglb.l ⊢ < ˙ = < K
tosglb.1 ⊢ φ → K ∈ Toset
tosglb.2 ⊢ φ → A ⊆ B
tosglb.e ⊢ ≤ ˙ = ≤ K
Assertion tosglblem ⊢ φ ∧ a ∈ B → ∀ b ∈ A a ≤ ˙ b ∧ ∀ c ∈ B ∀ b ∈ A c ≤ ˙ b → c ≤ ˙ a ↔ ∀ b ∈ A ¬ a < ˙ -1 b ∧ ∀ b ∈ B b < ˙ -1 a → ∃ d ∈ A b < ˙ -1 d

Proof

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