This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
toslub.l ⊢ < = ( lt ‘ 𝐾 )
toslub.1 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
toslub.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
toslub.e ⊢ ≤ = ( le ‘ 𝐾 )
Assertion toslublem ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) ) )

Proof

Step Hyp Ref Expression
1 toslub.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 toslub.l ⊢ < = ( lt ‘ 𝐾 )
3 toslub.1 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
4 toslub.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5 toslub.e ⊢ ≤ = ( le ‘ 𝐾 )
6 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐴 ) → 𝐾 ∈ Toset )
7 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐴 ) → 𝑎 ∈ 𝐵 )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 )
9 8 sselda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ 𝐵 )
10 1 5 2 tltnle ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑎 ) )
11 6 7 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 3expa ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐 ) )
20 19 con2bid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑏 ) )
21 16 20 syldan ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝑏 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑏 ) )
22 21 ralbidva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ∀ 𝑏 ∈ 𝐴 ¬ 𝑐 < 𝑏 ) )
23 breq2 ⊢ ( 𝑏 = 𝑑 → ( 𝑐 < 𝑏 ↔ 𝑐 < 𝑑 ) )
24 23 notbid ⊢ ( 𝑏 = 𝑑 → ( ¬ 𝑐 < 𝑏 ↔ ¬ 𝑐 < 𝑑 ) )
25 24 cbvralvw ⊢ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑐 < 𝑏 ↔ ∀ 𝑑 ∈ 𝐴 ¬ 𝑐 < 𝑑 )
26 ralnex ⊢ ( ∀ 𝑑 ∈ 𝐴 ¬ 𝑐 < 𝑑 ↔ ¬ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 )
27 25 26 bitri ⊢ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑐 < 𝑏 ↔ ¬ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 )
28 22 27 bitrdi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ¬ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) )
29 28 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ¬ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) )
30 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐾 ∈ Toset )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ 𝐵 )
32 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
33 1 5 2 tltnle ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑐 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑐 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑐 ) )
34 30 31 32 33 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑐 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑐 ) )
35 34 con2bid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑎 ) )
36 29 35 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ↔ ( ¬ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎 ) ) )
37 con34b ⊢ ( ( 𝑐 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) ↔ ( ¬ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎 ) )
38 36 37 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ↔ ( 𝑐 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) ) )
39 38 ralbidva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ↔ ∀ 𝑐 ∈ 𝐵 ( 𝑐 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) ) )
40 breq1 ⊢ ( 𝑏 = 𝑐 → ( 𝑏 < 𝑎 ↔ 𝑐 < 𝑎 ) )
41 breq1 ⊢ ( 𝑏 = 𝑐 → ( 𝑏 < 𝑑 ↔ 𝑐 < 𝑑 ) )
42 41 rexbidv ⊢ ( 𝑏 = 𝑐 → ( ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ↔ ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) )
43 40 42 imbi12d ⊢ ( 𝑏 = 𝑐 → ( ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ↔ ( 𝑐 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) ) )
44 43 cbvralvw ⊢ ( ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ↔ ∀ 𝑐 ∈ 𝐵 ( 𝑐 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑐 < 𝑑 ) )
45 39 44 bitr4di ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ↔ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) )
46 13 45 anbi12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) ) )