Step | Hyp | Ref
| Expression |
1 | | mgcval.2 |
. . 3
⊢ (𝜑 → 𝑉 ∈ Proset ) |
2 | | mgccole.1 |
. . . . . 6
⊢ (𝜑 → 𝐹𝐻𝐺) |
3 | | mgcoval.1 |
. . . . . . 7
⊢ 𝐴 = (Base‘𝑉) |
4 | | mgcoval.2 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑊) |
5 | | mgcoval.3 |
. . . . . . 7
⊢ ≤ =
(le‘𝑉) |
6 | | mgcoval.4 |
. . . . . . 7
⊢ ≲ =
(le‘𝑊) |
7 | | mgcval.1 |
. . . . . . 7
⊢ 𝐻 = (𝑉MGalConn𝑊) |
8 | | mgcval.3 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Proset ) |
9 | 3, 4, 5, 6, 7, 1, 8 | mgcval 30776 |
. . . . . 6
⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))))) |
10 | 2, 9 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))) |
11 | 10 | simplrd 770 |
. . . 4
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
12 | | mgccole2.1 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
13 | 11, 12 | ffvelrnd 6836 |
. . 3
⊢ (𝜑 → (𝐺‘𝑌) ∈ 𝐴) |
14 | 3, 5 | prsref 17593 |
. . 3
⊢ ((𝑉 ∈ Proset ∧ (𝐺‘𝑌) ∈ 𝐴) → (𝐺‘𝑌) ≤ (𝐺‘𝑌)) |
15 | 1, 13, 14 | syl2anc 588 |
. 2
⊢ (𝜑 → (𝐺‘𝑌) ≤ (𝐺‘𝑌)) |
16 | 10 | simprd 500 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))) |
17 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑌) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑌))) |
18 | 17 | breq1d 5035 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝑌) → ((𝐹‘𝑥) ≲ 𝑦 ↔ (𝐹‘(𝐺‘𝑌)) ≲ 𝑦)) |
19 | | breq1 5028 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝑌) → (𝑥 ≤ (𝐺‘𝑦) ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦))) |
20 | 18, 19 | bibi12d 350 |
. . . . . . 7
⊢ (𝑥 = (𝐺‘𝑌) → (((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) ↔ ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦)))) |
21 | 20 | adantl 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = (𝐺‘𝑌)) → (((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) ↔ ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦)))) |
22 | 21 | ralbidv 3124 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = (𝐺‘𝑌)) → (∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦)))) |
23 | 13, 22 | rspcdv 3531 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) → ∀𝑦 ∈ 𝐵 ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦)))) |
24 | 16, 23 | mpd 15 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦))) |
25 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) |
26 | 25 | breq2d 5037 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝑌) → ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐹‘(𝐺‘𝑌)) ≲ 𝑌)) |
27 | | fveq2 6651 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (𝐺‘𝑦) = (𝐺‘𝑌)) |
28 | 27 | adantl 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝑌) → (𝐺‘𝑦) = (𝐺‘𝑌)) |
29 | 28 | breq2d 5037 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝑌) → ((𝐺‘𝑌) ≤ (𝐺‘𝑦) ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑌))) |
30 | 26, 29 | bibi12d 350 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝑌) → (((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦)) ↔ ((𝐹‘(𝐺‘𝑌)) ≲ 𝑌 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑌)))) |
31 | 12, 30 | rspcdv 3531 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ((𝐹‘(𝐺‘𝑌)) ≲ 𝑦 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑦)) → ((𝐹‘(𝐺‘𝑌)) ≲ 𝑌 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑌)))) |
32 | 24, 31 | mpd 15 |
. 2
⊢ (𝜑 → ((𝐹‘(𝐺‘𝑌)) ≲ 𝑌 ↔ (𝐺‘𝑌) ≤ (𝐺‘𝑌))) |
33 | 15, 32 | mpbird 260 |
1
⊢ (𝜑 → (𝐹‘(𝐺‘𝑌)) ≲ 𝑌) |