Theorem mgcf1o 33663

Description: Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024.)

Hypotheses

Ref	Expression
mgcf1o.h	⊢ 𝐻 = (𝑉MGalConn𝑊)
mgcf1o.a	⊢ 𝐴 = (Base‘𝑉)
mgcf1o.b	⊢ 𝐵 = (Base‘𝑊)
mgcf1o.1	⊢ ≤ = (le‘𝑉)
mgcf1o.2	⊢ ≲ = (le‘𝑊)
mgcf1o.v	⊢ (𝜑 → 𝑉 ∈ Poset)
mgcf1o.w	⊢ (𝜑 → 𝑊 ∈ Poset)
mgcf1o.f	⊢ (𝜑 → 𝐹𝐻𝐺)

Assertion

Ref	Expression
mgcf1o	⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹))

Proof of Theorem mgcf1o

Dummy variables 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2763	. . . 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 18540	. . . . . . . . . 10 ⊢ (𝑉 ∈ Poset → 𝑉 ∈ Proset )
10	8, 9	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ Proset )
11		mgcf1o.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Poset)
12		posprs 18540	. . . . . . . . . 10 ⊢ (𝑊 ∈ Poset → 𝑊 ∈ Proset )
13	11, 12	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Proset )
14	3, 4, 5, 6, 7, 10, 13	dfmgc2 33656	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
15	2, 14	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))
16	15	simplld 780	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
17	16	ffnd 6740	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐴)
18	15	simplrd 782	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
19	18	frnd 6748	. . . . . 6 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
20	19	sselda 3913	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
21		fnfvelrn 7112	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ran 𝐹)
22	17, 20, 21	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → (𝐹‘𝑥) ∈ ran 𝐹)
23	18	ffnd 6740	. . . . 5 ⊢ (𝜑 → 𝐺 Fn 𝐵)
24	16	frnd 6748	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
25	24	sselda 3913	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ 𝐵)
26		fnfvelrn 7112	. . . . 5 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝐺‘𝑢) ∈ ran 𝐺)
27	23, 25, 26	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
28	8	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑉 ∈ Poset)
29	11	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑊 ∈ Poset)
30	2	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝐹𝐻𝐺)
31		simplr 781	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑦 ∈ 𝐴)
32	7, 3, 4, 5, 6, 28, 29, 30, 31	mgcf1olem1 33661	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑦))
33		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘𝑦) = 𝑢)
34	33	fveq2d 6920	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = (𝐺‘𝑢))
35		simpllr 788	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑥 = (𝐺‘𝑢))
36	34, 35	eqtr4d 2801	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = 𝑥)
37	36	fveq2d 6920	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑥))
38	32, 37, 33	3eqtr3rd 2807	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑢 = (𝐹‘𝑥))
39	17	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝐹 Fn 𝐴)
40		simplrr 790	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 ∈ ran 𝐹)
41		fvelrnb 6976	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢))
42	41	biimpa 482	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
43	39, 40, 42	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
44	38, 43	r19.29a 3174	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 = (𝐹‘𝑥))
45	8	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑉 ∈ Poset)
46	11	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑊 ∈ Poset)
47	2	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝐹𝐻𝐺)
48		simplr 781	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑣 ∈ 𝐵)
49	7, 3, 4, 5, 6, 45, 46, 47, 48	mgcf1olem2 33662	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
50		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘𝑣) = 𝑥)
51	50	fveq2d 6920	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑥))
52		simpllr 788	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑢 = (𝐹‘𝑥))
53	51, 52	eqtr4d 2801	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = 𝑢)
54	53	fveq2d 6920	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑢))
55	49, 54, 50	3eqtr3rd 2807	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑥 = (𝐺‘𝑢))
56	23	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝐺 Fn 𝐵)
57		simplrl 789	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 ∈ ran 𝐺)
58		fvelrnb 6976	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥))
59	58	biimpa 482	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
60	56, 57, 59	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
61	55, 60	r19.29a 3174	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 = (𝐺‘𝑢))
62	44, 61	impbida 813	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) → (𝑥 = (𝐺‘𝑢) ↔ 𝑢 = (𝐹‘𝑥)))
63	1, 22, 27, 62	f1o2d 7707	. . 3 ⊢ (𝜑 → (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺⟶1-1ontoran 𝐹)
64	16, 19	feqresmpt 6985	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) = (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)))
65	64	f1oeq1d 6849	. . 3 ⊢ (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶1-1ontoran 𝐹 ↔ (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺⟶1-1ontoran 𝐹))
66	63, 65	mpbird 260	. 2 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶1-1ontoran 𝐹)
67		simplll 787	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝜑)
68	19	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ran 𝐺 ⊆ 𝐴)
69		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺)
70	68, 69	sseldd 3914	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
71	70	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ∈ 𝐴)
72		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ ran 𝐺)
73	68, 72	sseldd 3914	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ 𝐴)
74	73	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴)
75		simpr 490	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦)
76	15	simprld 784	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))))
77	76	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
78	77	r19.21bi 3258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
79	78	r19.21bi 3258	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
80	79	imp 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
81	67, 71, 74, 75, 80	syl1111anc 854	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
82	69	fvresd 6936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
83	82	adantr 486	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
84	72	fvresd 6936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
85	84	adantr 486	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
86	81, 83, 85	3brtr4d 5143	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))
87	82, 84	breq12d 5121	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦) ↔ (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
88	87	biimpa 482	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
89	11	ad7antr 751	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑊 ∈ Poset)
90	8	ad7antr 751	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑉 ∈ Poset)
91	7, 10, 13, 2	mgcmnt2d 33658	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
92	91	ad7antr 751	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺 ∈ (𝑊Monot𝑉))
93	16	ad7antr 751	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹:𝐴⟶𝐵)
94	18	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺:𝐵⟶𝐴)
95		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑢 ∈ 𝐵)
96	94, 95	ffvelcdmd 7117	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ∈ 𝐴)
97	93, 96	ffvelcdmd 7117	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ∈ 𝐵)
98		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑣 ∈ 𝐵)
99	94, 98	ffvelcdmd 7117	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) ∈ 𝐴)
100	93, 99	ffvelcdmd 7117	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) ∈ 𝐵)
101		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
102	101	ad4antr 745	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
103		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) = 𝑥)
104	103	fveq2d 6920	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘𝑥))
105		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) = 𝑦)
106	105	fveq2d 6920	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑦))
107	102, 104, 106	3brtr4d 5143	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ≲ (𝐹‘(𝐺‘𝑣)))
108	4, 3, 6, 5, 89, 90, 92, 97, 100, 107	ismntd 33644	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) ≤ (𝐺‘(𝐹‘(𝐺‘𝑣))))
109	2	ad7antr 751	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹𝐻𝐺)
110	7, 3, 4, 5, 6, 90, 89, 109, 95	mgcf1olem2 33662	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) = (𝐺‘𝑢))
111	7, 3, 4, 5, 6, 90, 89, 109, 98	mgcf1olem2 33662	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
112	108, 110, 111	3brtr3d 5142	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ≤ (𝐺‘𝑣))
113	112, 103, 105	3brtr3d 5142	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑥 ≤ 𝑦)
114	23	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝐺 Fn 𝐵)
115	114	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝐺 Fn 𝐵)
116		simp-4r 796	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑦 ∈ ran 𝐺)
117		fvelrnb 6976	. . . . . . . . . 10 ⊢ (𝐺 Fn 𝐵 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦))
118	117	biimpa 482	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
119	115, 116, 118	syl2anc 596	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
120	113, 119	r19.29a 3174	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑥 ≤ 𝑦)
121		simpllr 788	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ∈ ran 𝐺)
122		fvelrnb 6976	. . . . . . . . 9 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥))
123	122	biimpa 482	. . . . . . . 8 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
124	114, 121, 123	syl2anc 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
125	120, 124	r19.29a 3174	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ≤ 𝑦)
126	88, 125	syldan 603	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → 𝑥 ≤ 𝑦)
127	86, 126	impbida 813	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
128	127	anasss 472	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
129	128	ralrimivva 3209	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
130		df-isom 6575	. 2 ⊢ ((𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹) ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶1-1ontoran 𝐹 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))))
131	66, 129, 130	sylanbrc 595	1 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   class class class wbr 5108   ↦ cmpt 5192  ran crn 5659   ↾ cres 5660   Fn wfn 6561  ⟶wf 6562  ⟶1-1ontowf1o 6565  ‘cfv 6566   Isom wiso 6567  (class class class)co 7451  Basecbs 17431  lecple 17479   Proset cproset 18516  Posetcpo 18531  Monotcmnt 33638  MGalConncmgc 33639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-ov 7454  df-oprab 7455  df-mpo 7456  df-map 8887  df-proset 18518  df-poset 18537  df-mnt 33640  df-mgc 33641

This theorem is used by:  nsgqusf1o  34071