Proof of Theorem mgcmntco
Step | Hyp | Ref
| Expression |
1 | | mgcmntco.3 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Proset ) |
2 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ Proset ) |
3 | | mgcval.2 |
. . . . . . 7
⊢ (𝜑 → 𝑉 ∈ Proset ) |
4 | | mgcmntco.4 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (𝑉Monot𝑋)) |
5 | | mgcoval.1 |
. . . . . . . 8
⊢ 𝐴 = (Base‘𝑉) |
6 | | mgcmntco.1 |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑋) |
7 | 5, 6 | mntf 30774 |
. . . . . . 7
⊢ ((𝑉 ∈ Proset ∧ 𝑋 ∈ Proset ∧ 𝐾 ∈ (𝑉Monot𝑋)) → 𝐾:𝐴⟶𝐶) |
8 | 3, 1, 4, 7 | syl3anc 1369 |
. . . . . 6
⊢ (𝜑 → 𝐾:𝐴⟶𝐶) |
9 | 8 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝐾:𝐴⟶𝐶) |
10 | | mgcoval.2 |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
11 | | mgcoval.3 |
. . . . . . . 8
⊢ ≤ =
(le‘𝑉) |
12 | | mgcoval.4 |
. . . . . . . 8
⊢ ≲ =
(le‘𝑊) |
13 | | mgcval.1 |
. . . . . . . 8
⊢ 𝐻 = (𝑉MGalConn𝑊) |
14 | | mgcval.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Proset ) |
15 | | mgccole.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹𝐻𝐺) |
16 | 5, 10, 11, 12, 13, 3, 14, 15 | mgcf2 30778 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
17 | 16 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) → 𝐺:𝐵⟶𝐴) |
18 | 17 | ffvelrnda 6835 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦) ∈ 𝐴) |
19 | 9, 18 | ffvelrnd 6836 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐾‘(𝐺‘𝑦)) ∈ 𝐶) |
20 | | mgcmntco.5 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (𝑊Monot𝑋)) |
21 | 10, 6 | mntf 30774 |
. . . . . . 7
⊢ ((𝑊 ∈ Proset ∧ 𝑋 ∈ Proset ∧ 𝐿 ∈ (𝑊Monot𝑋)) → 𝐿:𝐵⟶𝐶) |
22 | 14, 1, 20, 21 | syl3anc 1369 |
. . . . . 6
⊢ (𝜑 → 𝐿:𝐵⟶𝐶) |
23 | 22 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝐿:𝐵⟶𝐶) |
24 | 5, 10, 11, 12, 13, 3, 14, 15 | mgcf1 30777 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
25 | 24 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝐹:𝐴⟶𝐵) |
26 | 25, 18 | ffvelrnd 6836 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝐺‘𝑦)) ∈ 𝐵) |
27 | 23, 26 | ffvelrnd 6836 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐿‘(𝐹‘(𝐺‘𝑦))) ∈ 𝐶) |
28 | 22 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) → 𝐿:𝐵⟶𝐶) |
29 | 28 | ffvelrnda 6835 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐿‘𝑦) ∈ 𝐶) |
30 | 16 | ffvelrnda 6835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦) ∈ 𝐴) |
31 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑦) → (𝐾‘𝑥) = (𝐾‘(𝐺‘𝑦))) |
32 | | 2fveq3 6656 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑦) → (𝐿‘(𝐹‘𝑥)) = (𝐿‘(𝐹‘(𝐺‘𝑦)))) |
33 | 31, 32 | breq12d 5038 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝑦) → ((𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥)) ↔ (𝐾‘(𝐺‘𝑦)) < (𝐿‘(𝐹‘(𝐺‘𝑦))))) |
34 | 33 | adantl 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 = (𝐺‘𝑦)) → ((𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥)) ↔ (𝐾‘(𝐺‘𝑦)) < (𝐿‘(𝐹‘(𝐺‘𝑦))))) |
35 | 30, 34 | rspcdv 3531 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥)) → (𝐾‘(𝐺‘𝑦)) < (𝐿‘(𝐹‘(𝐺‘𝑦))))) |
36 | 35 | imp 411 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) → (𝐾‘(𝐺‘𝑦)) < (𝐿‘(𝐹‘(𝐺‘𝑦)))) |
37 | 36 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐾‘(𝐺‘𝑦)) < (𝐿‘(𝐹‘(𝐺‘𝑦)))) |
38 | | mgcmntco.2 |
. . . . 5
⊢ < =
(le‘𝑋) |
39 | 14 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝑊 ∈ Proset ) |
40 | 20 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝐿 ∈ (𝑊Monot𝑋)) |
41 | | simpr 489 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
42 | 3 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝑉 ∈ Proset ) |
43 | 15 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → 𝐹𝐻𝐺) |
44 | 5, 10, 11, 12, 13, 42, 39, 43, 41 | mgccole2 30780 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝐺‘𝑦)) ≲ 𝑦) |
45 | 10, 6, 12, 38, 39, 2, 40, 26, 41, 44 | ismntd 30773 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐿‘(𝐹‘(𝐺‘𝑦))) < (𝐿‘𝑦)) |
46 | 6, 38 | prstr 17594 |
. . . 4
⊢ ((𝑋 ∈ Proset ∧ ((𝐾‘(𝐺‘𝑦)) ∈ 𝐶 ∧ (𝐿‘(𝐹‘(𝐺‘𝑦))) ∈ 𝐶 ∧ (𝐿‘𝑦) ∈ 𝐶) ∧ ((𝐾‘(𝐺‘𝑦)) < (𝐿‘(𝐹‘(𝐺‘𝑦))) ∧ (𝐿‘(𝐹‘(𝐺‘𝑦))) < (𝐿‘𝑦))) → (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) |
47 | 2, 19, 27, 29, 37, 45, 46 | syl132anc 1386 |
. . 3
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) ∧ 𝑦 ∈ 𝐵) → (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) |
48 | 47 | ralrimiva 3111 |
. 2
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) → ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) |
49 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ Proset ) |
50 | 8 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝐾:𝐴⟶𝐶) |
51 | | simpr 489 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
52 | 50, 51 | ffvelrnd 6836 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐾‘𝑥) ∈ 𝐶) |
53 | 16 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝐺:𝐵⟶𝐴) |
54 | 24 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) → 𝐹:𝐴⟶𝐵) |
55 | 54 | ffvelrnda 6835 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
56 | 53, 55 | ffvelrnd 6836 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(𝐹‘𝑥)) ∈ 𝐴) |
57 | 50, 56 | ffvelrnd 6836 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐾‘(𝐺‘(𝐹‘𝑥))) ∈ 𝐶) |
58 | 22 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝐿:𝐵⟶𝐶) |
59 | 58, 55 | ffvelrnd 6836 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐿‘(𝐹‘𝑥)) ∈ 𝐶) |
60 | 3 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑉 ∈ Proset ) |
61 | 4 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ (𝑉Monot𝑋)) |
62 | 14 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑊 ∈ Proset ) |
63 | 15 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝐹𝐻𝐺) |
64 | 5, 10, 11, 12, 13, 60, 62, 63, 51 | mgccole1 30779 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥))) |
65 | 5, 6, 11, 38, 60, 49, 61, 51, 56, 64 | ismntd 30773 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐾‘𝑥) < (𝐾‘(𝐺‘(𝐹‘𝑥)))) |
66 | 24 | ffvelrnda 6835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
67 | | 2fveq3 6656 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (𝐾‘(𝐺‘𝑦)) = (𝐾‘(𝐺‘(𝐹‘𝑥)))) |
68 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (𝐿‘𝑦) = (𝐿‘(𝐹‘𝑥))) |
69 | 67, 68 | breq12d 5038 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦) ↔ (𝐾‘(𝐺‘(𝐹‘𝑥))) < (𝐿‘(𝐹‘𝑥)))) |
70 | 69 | adantl 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → ((𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦) ↔ (𝐾‘(𝐺‘(𝐹‘𝑥))) < (𝐿‘(𝐹‘𝑥)))) |
71 | 66, 70 | rspcdv 3531 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦) → (𝐾‘(𝐺‘(𝐹‘𝑥))) < (𝐿‘(𝐹‘𝑥)))) |
72 | 71 | imp 411 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) → (𝐾‘(𝐺‘(𝐹‘𝑥))) < (𝐿‘(𝐹‘𝑥))) |
73 | 72 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐾‘(𝐺‘(𝐹‘𝑥))) < (𝐿‘(𝐹‘𝑥))) |
74 | 6, 38 | prstr 17594 |
. . . 4
⊢ ((𝑋 ∈ Proset ∧ ((𝐾‘𝑥) ∈ 𝐶 ∧ (𝐾‘(𝐺‘(𝐹‘𝑥))) ∈ 𝐶 ∧ (𝐿‘(𝐹‘𝑥)) ∈ 𝐶) ∧ ((𝐾‘𝑥) < (𝐾‘(𝐺‘(𝐹‘𝑥))) ∧ (𝐾‘(𝐺‘(𝐹‘𝑥))) < (𝐿‘(𝐹‘𝑥)))) → (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) |
75 | 49, 52, 57, 59, 65, 73, 74 | syl132anc 1386 |
. . 3
⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) |
76 | 75 | ralrimiva 3111 |
. 2
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)) → ∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥))) |
77 | 48, 76 | impbida 801 |
1
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦))) |