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 31183

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 17949	. . . . . . . . . 10 ⊢ (𝑉 ∈ Poset → 𝑉 ∈ Proset )
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ Proset )
11		mgcf1o.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Poset)
12		posprs 17949	. . . . . . . . . 10 ⊢ (𝑊 ∈ Poset → 𝑊 ∈ Proset )
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Proset )
14	3, 4, 5, 6, 7, 10, 13	dfmgc2 31176	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
15	2, 14	mpbid 231	. . . . . . 7 ⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))
16	15	simplld 764	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
17	16	ffnd 6585	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐴)
18	15	simplrd 766	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
19	18	frnd 6592	. . . . . 6 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
20	19	sselda 3917	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
21		fnfvelrn 6940	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ran 𝐹)
22	17, 20, 21	syl2an2r 681	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → (𝐹‘𝑥) ∈ ran 𝐹)
23	18	ffnd 6585	. . . . 5 ⊢ (𝜑 → 𝐺 Fn 𝐵)
24	16	frnd 6592	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
25	24	sselda 3917	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ 𝐵)
26		fnfvelrn 6940	. . . . 5 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝐺‘𝑢) ∈ ran 𝐺)
27	23, 25, 26	syl2an2r 681	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
28	8	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑉 ∈ Poset)
29	11	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑊 ∈ Poset)
30	2	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝐹𝐻𝐺)
31		simplr 765	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑦 ∈ 𝐴)
32	7, 3, 4, 5, 6, 28, 29, 30, 31	mgcf1olem1 31181	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑦))
33		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘𝑦) = 𝑢)
34	33	fveq2d 6760	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = (𝐺‘𝑢))
35		simpllr 772	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑥 = (𝐺‘𝑢))
36	34, 35	eqtr4d 2781	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = 𝑥)
37	36	fveq2d 6760	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑥))
38	32, 37, 33	3eqtr3rd 2787	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑢 = (𝐹‘𝑥))
39	17	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝐹 Fn 𝐴)
40		simplrr 774	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 ∈ ran 𝐹)
41		fvelrnb 6812	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢))
42	41	biimpa 476	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
43	39, 40, 42	syl2anc 583	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
44	38, 43	r19.29a 3217	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 = (𝐹‘𝑥))
45	8	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑉 ∈ Poset)
46	11	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑊 ∈ Poset)
47	2	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝐹𝐻𝐺)
48		simplr 765	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑣 ∈ 𝐵)
49	7, 3, 4, 5, 6, 45, 46, 47, 48	mgcf1olem2 31182	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
50		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘𝑣) = 𝑥)
51	50	fveq2d 6760	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑥))
52		simpllr 772	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑢 = (𝐹‘𝑥))
53	51, 52	eqtr4d 2781	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = 𝑢)
54	53	fveq2d 6760	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑢))
55	49, 54, 50	3eqtr3rd 2787	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑥 = (𝐺‘𝑢))
56	23	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝐺 Fn 𝐵)
57		simplrl 773	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 ∈ ran 𝐺)
58		fvelrnb 6812	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥))
59	58	biimpa 476	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
60	56, 57, 59	syl2anc 583	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
61	55, 60	r19.29a 3217	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 = (𝐺‘𝑢))
62	44, 61	impbida 797	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) → (𝑥 = (𝐺‘𝑢) ↔ 𝑢 = (𝐹‘𝑥)))
63	1, 22, 27, 62	f1o2d 7501	. . 3 ⊢ (𝜑 → (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺–1-1-onto→ran 𝐹)
64	16, 19	feqresmpt 6820	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) = (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)))
65	64	f1oeq1d 6695	. . 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 771	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝜑)
68	19	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ran 𝐺 ⊆ 𝐴)
69		simplr 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺)
70	68, 69	sseldd 3918	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
71	70	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ∈ 𝐴)
72		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ ran 𝐺)
73	68, 72	sseldd 3918	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ 𝐴)
74	73	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴)
75		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦)
76	15	simprld 768	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))))
77	76	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
78	77	r19.21bi 3132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
79	78	r19.21bi 3132	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
80	79	imp 406	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
81	67, 71, 74, 75, 80	syl1111anc 836	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
82	69	fvresd 6776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
83	82	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
84	72	fvresd 6776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
85	84	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
86	81, 83, 85	3brtr4d 5102	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))
87	82, 84	breq12d 5083	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦) ↔ (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
88	87	biimpa 476	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
89	11	ad7antr 734	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑊 ∈ Poset)
90	8	ad7antr 734	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑉 ∈ Poset)
91	7, 10, 13, 2	mgcmnt2d 31178	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
92	91	ad7antr 734	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺 ∈ (𝑊Monot𝑉))
93	16	ad7antr 734	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹:𝐴⟶𝐵)
94	18	ad7antr 734	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺:𝐵⟶𝐴)
95		simp-4r 780	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑢 ∈ 𝐵)
96	94, 95	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ∈ 𝐴)
97	93, 96	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ∈ 𝐵)
98		simplr 765	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑣 ∈ 𝐵)
99	94, 98	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) ∈ 𝐴)
100	93, 99	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) ∈ 𝐵)
101		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
102	101	ad4antr 728	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
103		simpllr 772	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) = 𝑥)
104	103	fveq2d 6760	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘𝑥))
105		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) = 𝑦)
106	105	fveq2d 6760	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑦))
107	102, 104, 106	3brtr4d 5102	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ≲ (𝐹‘(𝐺‘𝑣)))
108	4, 3, 6, 5, 89, 90, 92, 97, 100, 107	ismntd 31164	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) ≤ (𝐺‘(𝐹‘(𝐺‘𝑣))))
109	2	ad7antr 734	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹𝐻𝐺)
110	7, 3, 4, 5, 6, 90, 89, 109, 95	mgcf1olem2 31182	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) = (𝐺‘𝑢))
111	7, 3, 4, 5, 6, 90, 89, 109, 98	mgcf1olem2 31182	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
112	108, 110, 111	3brtr3d 5101	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ≤ (𝐺‘𝑣))
113	112, 103, 105	3brtr3d 5101	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑥 ≤ 𝑦)
114	23	ad3antrrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝐺 Fn 𝐵)
115	114	ad2antrr 722	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝐺 Fn 𝐵)
116		simp-4r 780	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑦 ∈ ran 𝐺)
117		fvelrnb 6812	. . . . . . . . . 10 ⊢ (𝐺 Fn 𝐵 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦))
118	117	biimpa 476	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
119	115, 116, 118	syl2anc 583	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
120	113, 119	r19.29a 3217	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑥 ≤ 𝑦)
121		simpllr 772	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ∈ ran 𝐺)
122		fvelrnb 6812	. . . . . . . . 9 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥))
123	122	biimpa 476	. . . . . . . 8 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
124	114, 121, 123	syl2anc 583	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
125	120, 124	r19.29a 3217	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ≤ 𝑦)
126	88, 125	syldan 590	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → 𝑥 ≤ 𝑦)
127	86, 126	impbida 797	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
128	127	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
129	128	ralrimivva 3114	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
130		df-isom 6427	. 2 ⊢ ((𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹) ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran 𝐹 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))))
131	66, 129, 130	sylanbrc 582	1 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ∃wrex 3064 ⊆ wss 3883 class class class wbr 5070 ↦ cmpt 5153 ran crn 5581 ↾ cres 5582 Fn wfn 6413 ⟶wf 6414 –1-1-onto→wf1o 6417 ‘cfv 6418 Isom wiso 6419 (class class class)co 7255 Basecbs 16840 lecple 16895 Proset cproset 17926 Posetcpo 17940 Monotcmnt 31158 MGalConncmgc 31159

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-ov 7258 df-oprab 7259 df-mpo 7260 df-map 8575 df-proset 17928 df-poset 17946 df-mnt 31160 df-mgc 31161

This theorem is referenced by: nsgqusf1o 31503

W3C validator