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