mgcf1o - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mgcf1o		Structured version Visualization version GIF version

Theorem mgcf1o 31281

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 2738	. . . 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 18034	. . . . . . . . . 10 ⊢ (𝑉 ∈ Poset → 𝑉 ∈ Proset )
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ Proset )
11		mgcf1o.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Poset)
12		posprs 18034	. . . . . . . . . 10 ⊢ (𝑊 ∈ Poset → 𝑊 ∈ Proset )
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Proset )
14	3, 4, 5, 6, 7, 10, 13	dfmgc2 31274	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
15	2, 14	mpbid 231	. . . . . . 7 ⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))
16	15	simplld 765	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
17	16	ffnd 6601	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐴)
18	15	simplrd 767	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
19	18	frnd 6608	. . . . . 6 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
20	19	sselda 3921	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
21		fnfvelrn 6958	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ran 𝐹)
22	17, 20, 21	syl2an2r 682	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → (𝐹‘𝑥) ∈ ran 𝐹)
23	18	ffnd 6601	. . . . 5 ⊢ (𝜑 → 𝐺 Fn 𝐵)
24	16	frnd 6608	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
25	24	sselda 3921	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ 𝐵)
26		fnfvelrn 6958	. . . . 5 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝐺‘𝑢) ∈ ran 𝐺)
27	23, 25, 26	syl2an2r 682	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
28	8	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑉 ∈ Poset)
29	11	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑊 ∈ Poset)
30	2	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝐹𝐻𝐺)
31		simplr 766	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑦 ∈ 𝐴)
32	7, 3, 4, 5, 6, 28, 29, 30, 31	mgcf1olem1 31279	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑦))
33		simpr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘𝑦) = 𝑢)
34	33	fveq2d 6778	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = (𝐺‘𝑢))
35		simpllr 773	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑥 = (𝐺‘𝑢))
36	34, 35	eqtr4d 2781	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = 𝑥)
37	36	fveq2d 6778	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑥))
38	32, 37, 33	3eqtr3rd 2787	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑢 = (𝐹‘𝑥))
39	17	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝐹 Fn 𝐴)
40		simplrr 775	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 ∈ ran 𝐹)
41		fvelrnb 6830	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢))
42	41	biimpa 477	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
43	39, 40, 42	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
44	38, 43	r19.29a 3218	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 = (𝐹‘𝑥))
45	8	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑉 ∈ Poset)
46	11	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑊 ∈ Poset)
47	2	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝐹𝐻𝐺)
48		simplr 766	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑣 ∈ 𝐵)
49	7, 3, 4, 5, 6, 45, 46, 47, 48	mgcf1olem2 31280	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
50		simpr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘𝑣) = 𝑥)
51	50	fveq2d 6778	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑥))
52		simpllr 773	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑢 = (𝐹‘𝑥))
53	51, 52	eqtr4d 2781	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = 𝑢)
54	53	fveq2d 6778	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑢))
55	49, 54, 50	3eqtr3rd 2787	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑥 = (𝐺‘𝑢))
56	23	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝐺 Fn 𝐵)
57		simplrl 774	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 ∈ ran 𝐺)
58		fvelrnb 6830	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥))
59	58	biimpa 477	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
60	56, 57, 59	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
61	55, 60	r19.29a 3218	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 = (𝐺‘𝑢))
62	44, 61	impbida 798	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) → (𝑥 = (𝐺‘𝑢) ↔ 𝑢 = (𝐹‘𝑥)))
63	1, 22, 27, 62	f1o2d 7523	. . 3 ⊢ (𝜑 → (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺–1-1-onto→ran 𝐹)
64	16, 19	feqresmpt 6838	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) = (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)))
65	64	f1oeq1d 6711	. . 3 ⊢ (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹 ↔ (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺–1-1-onto→ran 𝐹))
66	63, 65	mpbird 256	. 2 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹)
67		simplll 772	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝜑)
68	19	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ran 𝐺 ⊆ 𝐴)
69		simplr 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺)
70	68, 69	sseldd 3922	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
71	70	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ∈ 𝐴)
72		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ ran 𝐺)
73	68, 72	sseldd 3922	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ 𝐴)
74	73	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴)
75		simpr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦)
76	15	simprld 769	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))))
77	76	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
78	77	r19.21bi 3134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
79	78	r19.21bi 3134	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
80	79	imp 407	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
81	67, 71, 74, 75, 80	syl1111anc 837	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
82	69	fvresd 6794	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
83	82	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
84	72	fvresd 6794	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
85	84	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
86	81, 83, 85	3brtr4d 5106	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))
87	82, 84	breq12d 5087	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦) ↔ (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
88	87	biimpa 477	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
89	11	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑊 ∈ Poset)
90	8	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑉 ∈ Poset)
91	7, 10, 13, 2	mgcmnt2d 31276	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
92	91	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺 ∈ (𝑊Monot𝑉))
93	16	ad7antr 735	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹:𝐴⟶𝐵)
94	18	ad7antr 735	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺:𝐵⟶𝐴)
95		simp-4r 781	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑢 ∈ 𝐵)
96	94, 95	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ∈ 𝐴)
97	93, 96	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ∈ 𝐵)
98		simplr 766	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑣 ∈ 𝐵)
99	94, 98	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) ∈ 𝐴)
100	93, 99	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) ∈ 𝐵)
101		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
102	101	ad4antr 729	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
103		simpllr 773	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) = 𝑥)
104	103	fveq2d 6778	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘𝑥))
105		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) = 𝑦)
106	105	fveq2d 6778	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑦))
107	102, 104, 106	3brtr4d 5106	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ≲ (𝐹‘(𝐺‘𝑣)))
108	4, 3, 6, 5, 89, 90, 92, 97, 100, 107	ismntd 31262	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) ≤ (𝐺‘(𝐹‘(𝐺‘𝑣))))
109	2	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹𝐻𝐺)
110	7, 3, 4, 5, 6, 90, 89, 109, 95	mgcf1olem2 31280	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) = (𝐺‘𝑢))
111	7, 3, 4, 5, 6, 90, 89, 109, 98	mgcf1olem2 31280	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
112	108, 110, 111	3brtr3d 5105	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ≤ (𝐺‘𝑣))
113	112, 103, 105	3brtr3d 5105	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑥 ≤ 𝑦)
114	23	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝐺 Fn 𝐵)
115	114	ad2antrr 723	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝐺 Fn 𝐵)
116		simp-4r 781	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑦 ∈ ran 𝐺)
117		fvelrnb 6830	. . . . . . . . . 10 ⊢ (𝐺 Fn 𝐵 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦))
118	117	biimpa 477	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
119	115, 116, 118	syl2anc 584	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
120	113, 119	r19.29a 3218	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑥 ≤ 𝑦)
121		simpllr 773	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ∈ ran 𝐺)
122		fvelrnb 6830	. . . . . . . . 9 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥))
123	122	biimpa 477	. . . . . . . 8 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
124	114, 121, 123	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
125	120, 124	r19.29a 3218	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ≤ 𝑦)
126	88, 125	syldan 591	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → 𝑥 ≤ 𝑦)
127	86, 126	impbida 798	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
128	127	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
129	128	ralrimivva 3123	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
130		df-isom 6442	. 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 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 ⊆ wss 3887 class class class wbr 5074 ↦ cmpt 5157 ran crn 5590 ↾ cres 5591 Fn wfn 6428 ⟶wf 6429 –1-1-onto→wf1o 6432 ‘cfv 6433 Isom wiso 6434 (class class class)co 7275 Basecbs 16912 lecple 16969 Proset cproset 18011 Posetcpo 18025 Monotcmnt 31256 MGalConncmgc 31257

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-ov 7278 df-oprab 7279 df-mpo 7280 df-map 8617 df-proset 18013 df-poset 18031 df-mnt 31258 df-mgc 31259

This theorem is referenced by: nsgqusf1o 31601

W3C validator