| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢ (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)) = (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)) | 
| 2 |  | mgcf1o.f | . . . . . . . 8
⊢ (𝜑 → 𝐹𝐻𝐺) | 
| 3 |  | mgcf1o.a | . . . . . . . . 9
⊢ 𝐴 = (Base‘𝑉) | 
| 4 |  | mgcf1o.b | . . . . . . . . 9
⊢ 𝐵 = (Base‘𝑊) | 
| 5 |  | mgcf1o.1 | . . . . . . . . 9
⊢  ≤ =
(le‘𝑉) | 
| 6 |  | mgcf1o.2 | . . . . . . . . 9
⊢  ≲ =
(le‘𝑊) | 
| 7 |  | mgcf1o.h | . . . . . . . . 9
⊢ 𝐻 = (𝑉MGalConn𝑊) | 
| 8 |  | mgcf1o.v | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ Poset) | 
| 9 |  | posprs 18362 | . . . . . . . . . 10
⊢ (𝑉 ∈ Poset → 𝑉 ∈ Proset
) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ Proset ) | 
| 11 |  | mgcf1o.w | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ Poset) | 
| 12 |  | posprs 18362 | . . . . . . . . . 10
⊢ (𝑊 ∈ Poset → 𝑊 ∈ Proset
) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Proset ) | 
| 14 | 3, 4, 5, 6, 7, 10,
13 | dfmgc2 32986 | . . . . . . . 8
⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))) | 
| 15 | 2, 14 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))) | 
| 16 | 15 | simplld 768 | . . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 17 | 16 | ffnd 6737 | . . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 18 | 15 | simplrd 770 | . . . . . . 7
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 19 | 18 | frnd 6744 | . . . . . 6
⊢ (𝜑 → ran 𝐺 ⊆ 𝐴) | 
| 20 | 19 | sselda 3983 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → 𝑥 ∈ 𝐴) | 
| 21 |  | fnfvelrn 7100 | . . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ran 𝐹) | 
| 22 | 17, 20, 21 | syl2an2r 685 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → (𝐹‘𝑥) ∈ ran 𝐹) | 
| 23 | 18 | ffnd 6737 | . . . . 5
⊢ (𝜑 → 𝐺 Fn 𝐵) | 
| 24 | 16 | frnd 6744 | . . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) | 
| 25 | 24 | sselda 3983 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ 𝐵) | 
| 26 |  | fnfvelrn 7100 | . . . . 5
⊢ ((𝐺 Fn 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝐺‘𝑢) ∈ ran 𝐺) | 
| 27 | 23, 25, 26 | syl2an2r 685 | . . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺) | 
| 28 | 8 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑉 ∈ Poset) | 
| 29 | 11 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑊 ∈ Poset) | 
| 30 | 2 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝐹𝐻𝐺) | 
| 31 |  | simplr 769 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑦 ∈ 𝐴) | 
| 32 | 7, 3, 4, 5, 6, 28,
29, 30, 31 | mgcf1olem1 32991 | . . . . . . 7
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑦)) | 
| 33 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘𝑦) = 𝑢) | 
| 34 | 33 | fveq2d 6910 | . . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = (𝐺‘𝑢)) | 
| 35 |  | simpllr 776 | . . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑥 = (𝐺‘𝑢)) | 
| 36 | 34, 35 | eqtr4d 2780 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = 𝑥) | 
| 37 | 36 | fveq2d 6910 | . . . . . . 7
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑥)) | 
| 38 | 32, 37, 33 | 3eqtr3rd 2786 | . . . . . 6
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑢 = (𝐹‘𝑥)) | 
| 39 | 17 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝐹 Fn 𝐴) | 
| 40 |  | simplrr 778 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 ∈ ran 𝐹) | 
| 41 |  | fvelrnb 6969 | . . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)) | 
| 42 | 41 | biimpa 476 | . . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢) | 
| 43 | 39, 40, 42 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢) | 
| 44 | 38, 43 | r19.29a 3162 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 = (𝐹‘𝑥)) | 
| 45 | 8 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑉 ∈ Poset) | 
| 46 | 11 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑊 ∈ Poset) | 
| 47 | 2 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝐹𝐻𝐺) | 
| 48 |  | simplr 769 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑣 ∈ 𝐵) | 
| 49 | 7, 3, 4, 5, 6, 45,
46, 47, 48 | mgcf1olem2 32992 | . . . . . . 7
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣)) | 
| 50 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘𝑣) = 𝑥) | 
| 51 | 50 | fveq2d 6910 | . . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑥)) | 
| 52 |  | simpllr 776 | . . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑢 = (𝐹‘𝑥)) | 
| 53 | 51, 52 | eqtr4d 2780 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = 𝑢) | 
| 54 | 53 | fveq2d 6910 | . . . . . . 7
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑢)) | 
| 55 | 49, 54, 50 | 3eqtr3rd 2786 | . . . . . 6
⊢
(((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑥 = (𝐺‘𝑢)) | 
| 56 | 23 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝐺 Fn 𝐵) | 
| 57 |  | simplrl 777 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 ∈ ran 𝐺) | 
| 58 |  | fvelrnb 6969 | . . . . . . . 8
⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)) | 
| 59 | 58 | biimpa 476 | . . . . . . 7
⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥) | 
| 60 | 56, 57, 59 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥) | 
| 61 | 55, 60 | r19.29a 3162 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 = (𝐺‘𝑢)) | 
| 62 | 44, 61 | impbida 801 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) → (𝑥 = (𝐺‘𝑢) ↔ 𝑢 = (𝐹‘𝑥))) | 
| 63 | 1, 22, 27, 62 | f1o2d 7687 | . . 3
⊢ (𝜑 → (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺–1-1-onto→ran
𝐹) | 
| 64 | 16, 19 | feqresmpt 6978 | . . . 4
⊢ (𝜑 → (𝐹 ↾ ran 𝐺) = (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥))) | 
| 65 | 64 | f1oeq1d 6843 | . . 3
⊢ (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹 ↔ (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺–1-1-onto→ran
𝐹)) | 
| 66 | 63, 65 | mpbird 257 | . 2
⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹) | 
| 67 |  | simplll 775 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝜑) | 
| 68 | 19 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ran 𝐺 ⊆ 𝐴) | 
| 69 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺) | 
| 70 | 68, 69 | sseldd 3984 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ 𝐴) | 
| 71 | 70 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ∈ 𝐴) | 
| 72 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ ran 𝐺) | 
| 73 | 68, 72 | sseldd 3984 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ 𝐴) | 
| 74 | 73 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴) | 
| 75 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦) | 
| 76 | 15 | simprld 772 | . . . . . . . . . . 11
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))) | 
| 77 | 76 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))) | 
| 78 | 77 | r19.21bi 3251 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))) | 
| 79 | 78 | r19.21bi 3251 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))) | 
| 80 | 79 | imp 406 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) | 
| 81 | 67, 71, 74, 75, 80 | syl1111anc 841 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) | 
| 82 | 69 | fvresd 6926 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥)) | 
| 83 | 82 | adantr 480 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥)) | 
| 84 | 72 | fvresd 6926 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦)) | 
| 85 | 84 | adantr 480 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦)) | 
| 86 | 81, 83, 85 | 3brtr4d 5175 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) | 
| 87 | 82, 84 | breq12d 5156 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦) ↔ (𝐹‘𝑥) ≲ (𝐹‘𝑦))) | 
| 88 | 87 | biimpa 476 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) | 
| 89 | 11 | ad7antr 738 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑊 ∈ Poset) | 
| 90 | 8 | ad7antr 738 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑉 ∈ Poset) | 
| 91 | 7, 10, 13, 2 | mgcmnt2d 32988 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉)) | 
| 92 | 91 | ad7antr 738 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺 ∈ (𝑊Monot𝑉)) | 
| 93 | 16 | ad7antr 738 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹:𝐴⟶𝐵) | 
| 94 | 18 | ad7antr 738 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺:𝐵⟶𝐴) | 
| 95 |  | simp-4r 784 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑢 ∈ 𝐵) | 
| 96 | 94, 95 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ∈ 𝐴) | 
| 97 | 93, 96 | ffvelcdmd 7105 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ∈ 𝐵) | 
| 98 |  | simplr 769 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑣 ∈ 𝐵) | 
| 99 | 94, 98 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) ∈ 𝐴) | 
| 100 | 93, 99 | ffvelcdmd 7105 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) ∈ 𝐵) | 
| 101 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) | 
| 102 | 101 | ad4antr 732 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) | 
| 103 |  | simpllr 776 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) = 𝑥) | 
| 104 | 103 | fveq2d 6910 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘𝑥)) | 
| 105 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) = 𝑦) | 
| 106 | 105 | fveq2d 6910 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑦)) | 
| 107 | 102, 104,
106 | 3brtr4d 5175 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ≲ (𝐹‘(𝐺‘𝑣))) | 
| 108 | 4, 3, 6, 5, 89, 90, 92, 97, 100, 107 | ismntd 32974 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) ≤ (𝐺‘(𝐹‘(𝐺‘𝑣)))) | 
| 109 | 2 | ad7antr 738 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹𝐻𝐺) | 
| 110 | 7, 3, 4, 5, 6, 90,
89, 109, 95 | mgcf1olem2 32992 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) = (𝐺‘𝑢)) | 
| 111 | 7, 3, 4, 5, 6, 90,
89, 109, 98 | mgcf1olem2 32992 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣)) | 
| 112 | 108, 110,
111 | 3brtr3d 5174 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) | 
| 113 | 112, 103,
105 | 3brtr3d 5174 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑥 ≤ 𝑦) | 
| 114 | 23 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝐺 Fn 𝐵) | 
| 115 | 114 | ad2antrr 726 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝐺 Fn 𝐵) | 
| 116 |  | simp-4r 784 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑦 ∈ ran 𝐺) | 
| 117 |  | fvelrnb 6969 | . . . . . . . . . 10
⊢ (𝐺 Fn 𝐵 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)) | 
| 118 | 117 | biimpa 476 | . . . . . . . . 9
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦) | 
| 119 | 115, 116,
118 | syl2anc 584 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦) | 
| 120 | 113, 119 | r19.29a 3162 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑥 ≤ 𝑦) | 
| 121 |  | simpllr 776 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ∈ ran 𝐺) | 
| 122 |  | fvelrnb 6969 | . . . . . . . . 9
⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)) | 
| 123 | 122 | biimpa 476 | . . . . . . . 8
⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥) | 
| 124 | 114, 121,
123 | syl2anc 584 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥) | 
| 125 | 120, 124 | r19.29a 3162 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ≤ 𝑦) | 
| 126 | 88, 125 | syldan 591 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → 𝑥 ≤ 𝑦) | 
| 127 | 86, 126 | impbida 801 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))) | 
| 128 | 127 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))) | 
| 129 | 128 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))) | 
| 130 |  | df-isom 6570 | . 2
⊢ ((𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹) ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))) | 
| 131 | 66, 129, 130 | sylanbrc 583 | 1
⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹)) |