Metamath Proof Explorer

Theorem toslublem

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

Ref Expression
Hypotheses toslub.b ⊢ B = Base K
toslub.l ⊢ < ˙ = < K
toslub.1 ⊢ φ → K ∈ Toset
toslub.2 ⊢ φ → A ⊆ B
toslub.e ⊢ ≤ ˙ = ≤ K
Assertion toslublem ⊢ φ ∧ a ∈ B → ∀ b ∈ A b ≤ ˙ a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ ˙ c → a ≤ ˙ c ↔ ∀ b ∈ A ¬ a < ˙ b ∧ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d

Proof

Step Hyp Ref Expression
1 toslub.b ⊢ B = Base K
2 toslub.l ⊢ < ˙ = < K
3 toslub.1 ⊢ φ → K ∈ Toset
4 toslub.2 ⊢ φ → A ⊆ B
5 toslub.e ⊢ ≤ ˙ = ≤ K
6 3 ad2antrr ⊢ φ ∧ a ∈ B ∧ b ∈ A → K ∈ Toset
7 simplr ⊢ φ ∧ a ∈ B ∧ b ∈ A → a ∈ B
8 4 adantr ⊢ φ ∧ a ∈ B → A ⊆ B
9 8 sselda ⊢ φ ∧ a ∈ B ∧ b ∈ A → b ∈ B
10 1 5 2 tltnle ⊢ K ∈ Toset ∧ a ∈ B ∧ b ∈ B → a < ˙ b ↔ ¬ b ≤ ˙ a
11 6 7 9 10 syl3anc ⊢ φ ∧ a ∈ B ∧ b ∈ A → a < ˙ b ↔ ¬ b ≤ ˙ a
12 11 con2bid ⊢ φ ∧ a ∈ B ∧ b ∈ A → b ≤ ˙ a ↔ ¬ a < ˙ b
13 12 ralbidva ⊢ φ ∧ a ∈ B → ∀ b ∈ A b ≤ ˙ a ↔ ∀ b ∈ A ¬ a < ˙ b
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 ∧ c ∈ B ∧ b ∈ B → c < ˙ b ↔ ¬ b ≤ ˙ c
18 3 17 syl3an1 ⊢ φ ∧ c ∈ B ∧ b ∈ B → c < ˙ b ↔ ¬ b ≤ ˙ c
19 18 3expa ⊢ φ ∧ c ∈ B ∧ b ∈ B → c < ˙ b ↔ ¬ b ≤ ˙ c
20 19 con2bid ⊢ φ ∧ c ∈ B ∧ b ∈ B → b ≤ ˙ c ↔ ¬ c < ˙ b
21 16 20 syldan ⊢ φ ∧ c ∈ B ∧ b ∈ A → b ≤ ˙ c ↔ ¬ c < ˙ b
22 21 ralbidva ⊢ φ ∧ c ∈ B → ∀ b ∈ A b ≤ ˙ c ↔ ∀ b ∈ A ¬ c < ˙ b
23 breq2 ⊢ b = d → c < ˙ b ↔ c < ˙ d
24 23 notbid ⊢ b = d → ¬ c < ˙ b ↔ ¬ c < ˙ d
25 24 cbvralvw ⊢ ∀ b ∈ A ¬ c < ˙ b ↔ ∀ d ∈ A ¬ c < ˙ d
26 ralnex ⊢ ∀ d ∈ A ¬ c < ˙ d ↔ ¬ ∃ d ∈ A c < ˙ d
27 25 26 bitri ⊢ ∀ b ∈ A ¬ c < ˙ b ↔ ¬ ∃ d ∈ A c < ˙ d
28 22 27 bitrdi ⊢ φ ∧ c ∈ B → ∀ b ∈ A b ≤ ˙ c ↔ ¬ ∃ d ∈ A c < ˙ d
29 28 adantlr ⊢ φ ∧ a ∈ B ∧ c ∈ B → ∀ b ∈ A b ≤ ˙ c ↔ ¬ ∃ d ∈ A c < ˙ d
30 3 ad2antrr ⊢ φ ∧ a ∈ B ∧ c ∈ B → K ∈ Toset
31 simpr ⊢ φ ∧ a ∈ B ∧ c ∈ B → c ∈ B
32 simplr ⊢ φ ∧ a ∈ B ∧ c ∈ B → a ∈ B
33 1 5 2 tltnle ⊢ K ∈ Toset ∧ c ∈ B ∧ a ∈ B → c < ˙ a ↔ ¬ a ≤ ˙ c
34 30 31 32 33 syl3anc ⊢ φ ∧ a ∈ B ∧ c ∈ B → c < ˙ a ↔ ¬ a ≤ ˙ c
35 34 con2bid ⊢ φ ∧ a ∈ B ∧ c ∈ B → a ≤ ˙ c ↔ ¬ c < ˙ a
36 29 35 imbi12d ⊢ φ ∧ a ∈ B ∧ c ∈ B → ∀ b ∈ A b ≤ ˙ c → a ≤ ˙ c ↔ ¬ ∃ d ∈ A c < ˙ d → ¬ c < ˙ a
37 con34b ⊢ c < ˙ a → ∃ d ∈ A c < ˙ d ↔ ¬ ∃ d ∈ A c < ˙ d → ¬ c < ˙ a
38 36 37 bitr4di ⊢ φ ∧ a ∈ B ∧ c ∈ B → ∀ b ∈ A b ≤ ˙ c → a ≤ ˙ c ↔ c < ˙ a → ∃ d ∈ A c < ˙ d
39 38 ralbidva ⊢ φ ∧ a ∈ B → ∀ c ∈ B ∀ b ∈ A b ≤ ˙ c → a ≤ ˙ c ↔ ∀ c ∈ B c < ˙ a → ∃ d ∈ A c < ˙ d
40 breq1 ⊢ b = c → b < ˙ a ↔ c < ˙ a
41 breq1 ⊢ b = c → b < ˙ d ↔ c < ˙ d
42 41 rexbidv ⊢ b = c → ∃ d ∈ A b < ˙ d ↔ ∃ d ∈ A c < ˙ d
43 40 42 imbi12d ⊢ b = c → b < ˙ a → ∃ d ∈ A b < ˙ d ↔ c < ˙ a → ∃ d ∈ A c < ˙ d
44 43 cbvralvw ⊢ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d ↔ ∀ c ∈ B c < ˙ a → ∃ d ∈ A c < ˙ d
45 39 44 bitr4di ⊢ φ ∧ a ∈ B → ∀ c ∈ B ∀ b ∈ A b ≤ ˙ c → a ≤ ˙ c ↔ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d
46 13 45 anbi12d ⊢ φ ∧ a ∈ B → ∀ b ∈ A b ≤ ˙ a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ ˙ c → a ≤ ˙ c ↔ ∀ b ∈ A ¬ a < ˙ b ∧ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d