Proof of Theorem tosglblem
Step | Hyp | Ref
| Expression |
1 | | tosglb.1 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Toset) |
2 | 1 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐾 ∈ Toset) |
3 | | tosglb.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐴 ⊆ 𝐵) |
5 | 4 | sselda 3922 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
6 | | simplr 766 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑎 ∈ 𝐵) |
7 | | tosglb.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
8 | | tosglb.e |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
9 | | tosglb.l |
. . . . . . 7
⊢ < =
(lt‘𝐾) |
10 | 7, 8, 9 | tltnle 18129 |
. . . . . 6
⊢ ((𝐾 ∈ Toset ∧ 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) → (𝑏 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑏)) |
11 | 2, 5, 6, 10 | syl3anc 1370 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑏 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑏)) |
12 | 11 | con2bid 355 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑎 ≤ 𝑏 ↔ ¬ 𝑏 < 𝑎)) |
13 | 12 | ralbidva 3117 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎)) |
14 | 3 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
15 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) |
16 | 14, 15 | sseldd 3923 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
17 | 7, 8, 9 | tltnle 18129 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Toset ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) |
18 | 1, 17 | syl3an1 1162 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) |
19 | 18 | 3com23 1125 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) |
20 | 19 | 3expa 1117 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) |
21 | 20 | con2bid 355 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑐 ≤ 𝑏 ↔ ¬ 𝑏 < 𝑐)) |
22 | 16, 21 | syldan 591 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑐 ≤ 𝑏 ↔ ¬ 𝑏 < 𝑐)) |
23 | 22 | ralbidva 3117 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑐)) |
24 | | breq1 5078 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑑 → (𝑏 < 𝑐 ↔ 𝑑 < 𝑐)) |
25 | 24 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (¬ 𝑏 < 𝑐 ↔ ¬ 𝑑 < 𝑐)) |
26 | 25 | cbvralvw 3382 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑏 < 𝑐 ↔ ∀𝑑 ∈ 𝐴 ¬ 𝑑 < 𝑐) |
27 | | ralnex 3166 |
. . . . . . . . . 10
⊢
(∀𝑑 ∈
𝐴 ¬ 𝑑 < 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐) |
28 | 26, 27 | bitri 274 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑏 < 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐) |
29 | 23, 28 | bitrdi 287 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) |
30 | 29 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) |
31 | 1 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝐾 ∈ Toset) |
32 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
33 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) |
34 | 7, 8, 9 | tltnle 18129 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Toset ∧ 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑎)) |
35 | 31, 32, 33, 34 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑎)) |
36 | 35 | con2bid 355 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑐 ≤ 𝑎 ↔ ¬ 𝑎 < 𝑐)) |
37 | 30, 36 | imbi12d 345 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐))) |
38 | | con34b 316 |
. . . . . 6
⊢ ((𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐)) |
39 | 37, 38 | bitr4di 289 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐))) |
40 | 39 | ralbidva 3117 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ ∀𝑐 ∈ 𝐵 (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐))) |
41 | | breq2 5079 |
. . . . . 6
⊢ (𝑏 = 𝑐 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑐)) |
42 | | breq2 5079 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → (𝑑 < 𝑏 ↔ 𝑑 < 𝑐)) |
43 | 42 | rexbidv 3225 |
. . . . . 6
⊢ (𝑏 = 𝑐 → (∃𝑑 ∈ 𝐴 𝑑 < 𝑏 ↔ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) |
44 | 41, 43 | imbi12d 345 |
. . . . 5
⊢ (𝑏 = 𝑐 → ((𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏) ↔ (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐))) |
45 | 44 | cbvralvw 3382 |
. . . 4
⊢
(∀𝑏 ∈
𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏) ↔ ∀𝑐 ∈ 𝐵 (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) |
46 | 40, 45 | bitr4di 289 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏))) |
47 | 13, 46 | anbi12d 631 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏)))) |
48 | | vex 3435 |
. . . . . 6
⊢ 𝑎 ∈ V |
49 | | vex 3435 |
. . . . . 6
⊢ 𝑏 ∈ V |
50 | 48, 49 | brcnv 5786 |
. . . . 5
⊢ (𝑎◡ < 𝑏 ↔ 𝑏 < 𝑎) |
51 | 50 | notbii 320 |
. . . 4
⊢ (¬
𝑎◡ < 𝑏 ↔ ¬ 𝑏 < 𝑎) |
52 | 51 | ralbii 3092 |
. . 3
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑎◡
<
𝑏 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎) |
53 | 49, 48 | brcnv 5786 |
. . . . 5
⊢ (𝑏◡ < 𝑎 ↔ 𝑎 < 𝑏) |
54 | | vex 3435 |
. . . . . . 7
⊢ 𝑑 ∈ V |
55 | 49, 54 | brcnv 5786 |
. . . . . 6
⊢ (𝑏◡ < 𝑑 ↔ 𝑑 < 𝑏) |
56 | 55 | rexbii 3180 |
. . . . 5
⊢
(∃𝑑 ∈
𝐴 𝑏◡
<
𝑑 ↔ ∃𝑑 ∈ 𝐴 𝑑 < 𝑏) |
57 | 53, 56 | imbi12i 351 |
. . . 4
⊢ ((𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑) ↔ (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏)) |
58 | 57 | ralbii 3092 |
. . 3
⊢
(∀𝑏 ∈
𝐵 (𝑏◡
<
𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑) ↔ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏)) |
59 | 52, 58 | anbi12i 627 |
. 2
⊢
((∀𝑏 ∈
𝐴 ¬ 𝑎◡
<
𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡
<
𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏))) |
60 | 47, 59 | bitr4di 289 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡
<
𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡
<
𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑)))) |