| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mgcval.2 | . . 3
⊢ (𝜑 → 𝑉 ∈ Proset ) | 
| 2 |  | mgcmnt1.1 | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝐴) | 
| 3 |  | mgcmnt1.2 | . . 3
⊢ (𝜑 → 𝑌 ∈ 𝐴) | 
| 4 |  | mgccole.1 | . . . . . 6
⊢ (𝜑 → 𝐹𝐻𝐺) | 
| 5 |  | mgcoval.1 | . . . . . . 7
⊢ 𝐴 = (Base‘𝑉) | 
| 6 |  | mgcoval.2 | . . . . . . 7
⊢ 𝐵 = (Base‘𝑊) | 
| 7 |  | mgcoval.3 | . . . . . . 7
⊢  ≤ =
(le‘𝑉) | 
| 8 |  | mgcoval.4 | . . . . . . 7
⊢  ≲ =
(le‘𝑊) | 
| 9 |  | mgcval.1 | . . . . . . 7
⊢ 𝐻 = (𝑉MGalConn𝑊) | 
| 10 |  | mgcval.3 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Proset ) | 
| 11 | 5, 6, 7, 8, 9, 1, 10 | mgcval 32977 | . . . . . 6
⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))))) | 
| 12 | 4, 11 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))) | 
| 13 | 12 | simplrd 770 | . . . 4
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 14 | 12 | simplld 768 | . . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 15 | 14, 3 | ffvelcdmd 7105 | . . . 4
⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝐵) | 
| 16 | 13, 15 | ffvelcdmd 7105 | . . 3
⊢ (𝜑 → (𝐺‘(𝐹‘𝑌)) ∈ 𝐴) | 
| 17 |  | mgcmnt1.3 | . . 3
⊢ (𝜑 → 𝑋 ≤ 𝑌) | 
| 18 | 5, 6, 7, 8, 9, 1, 10, 4, 3 | mgccole1 32980 | . . 3
⊢ (𝜑 → 𝑌 ≤ (𝐺‘(𝐹‘𝑌))) | 
| 19 | 5, 7 | prstr 18345 | . . 3
⊢ ((𝑉 ∈ Proset ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ (𝐺‘(𝐹‘𝑌)) ∈ 𝐴) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ (𝐺‘(𝐹‘𝑌)))) → 𝑋 ≤ (𝐺‘(𝐹‘𝑌))) | 
| 20 | 1, 2, 3, 16, 17, 18, 19 | syl132anc 1390 | . 2
⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑌))) | 
| 21 | 12 | simprd 495 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))) | 
| 22 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) | 
| 23 | 22 | breq1d 5153 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≲ 𝑦 ↔ (𝐹‘𝑋) ≲ 𝑦)) | 
| 24 |  | breq1 5146 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 ≤ (𝐺‘𝑦) ↔ 𝑋 ≤ (𝐺‘𝑦))) | 
| 25 | 23, 24 | bibi12d 345 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) ↔ ((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦)))) | 
| 26 | 25 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) ↔ ((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦)))) | 
| 27 | 26 | ralbidv 3178 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦)))) | 
| 28 | 2, 27 | rspcdv 3614 | . . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)) → ∀𝑦 ∈ 𝐵 ((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦)))) | 
| 29 | 21, 28 | mpd 15 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦))) | 
| 30 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑌)) → 𝑦 = (𝐹‘𝑌)) | 
| 31 | 30 | breq2d 5155 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑌)) → ((𝐹‘𝑋) ≲ 𝑦 ↔ (𝐹‘𝑋) ≲ (𝐹‘𝑌))) | 
| 32 | 30 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑌)) → (𝐺‘𝑦) = (𝐺‘(𝐹‘𝑌))) | 
| 33 | 32 | breq2d 5155 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑌)) → (𝑋 ≤ (𝐺‘𝑦) ↔ 𝑋 ≤ (𝐺‘(𝐹‘𝑌)))) | 
| 34 | 31, 33 | bibi12d 345 | . . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑌)) → (((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦)) ↔ ((𝐹‘𝑋) ≲ (𝐹‘𝑌) ↔ 𝑋 ≤ (𝐺‘(𝐹‘𝑌))))) | 
| 35 | 15, 34 | rspcdv 3614 | . . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ((𝐹‘𝑋) ≲ 𝑦 ↔ 𝑋 ≤ (𝐺‘𝑦)) → ((𝐹‘𝑋) ≲ (𝐹‘𝑌) ↔ 𝑋 ≤ (𝐺‘(𝐹‘𝑌))))) | 
| 36 | 29, 35 | mpd 15 | . 2
⊢ (𝜑 → ((𝐹‘𝑋) ≲ (𝐹‘𝑌) ↔ 𝑋 ≤ (𝐺‘(𝐹‘𝑌)))) | 
| 37 | 20, 36 | mpbird 257 | 1
⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌)) |