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 31863

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 2736	. . . 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 18205	. . . . . . . . . 10 ⊢ (𝑉 ∈ Poset → 𝑉 ∈ Proset )
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ Proset )
11		mgcf1o.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Poset)
12		posprs 18205	. . . . . . . . . 10 ⊢ (𝑊 ∈ Poset → 𝑊 ∈ Proset )
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Proset )
14	3, 4, 5, 6, 7, 10, 13	dfmgc2 31856	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
15	2, 14	mpbid 231	. . . . . . 7 ⊢ (𝜑 → ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))
16	15	simplld 766	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
17	16	ffnd 6669	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐴)
18	15	simplrd 768	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
19	18	frnd 6676	. . . . . 6 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐴)
20	19	sselda 3944	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
21		fnfvelrn 7031	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ran 𝐹)
22	17, 20, 21	syl2an2r 683	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐺) → (𝐹‘𝑥) ∈ ran 𝐹)
23	18	ffnd 6669	. . . . 5 ⊢ (𝜑 → 𝐺 Fn 𝐵)
24	16	frnd 6676	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
25	24	sselda 3944	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ 𝐵)
26		fnfvelrn 7031	. . . . 5 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝐺‘𝑢) ∈ ran 𝐺)
27	23, 25, 26	syl2an2r 683	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺)
28	8	ad4antr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑉 ∈ Poset)
29	11	ad4antr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑊 ∈ Poset)
30	2	ad4antr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝐹𝐻𝐺)
31		simplr 767	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑦 ∈ 𝐴)
32	7, 3, 4, 5, 6, 28, 29, 30, 31	mgcf1olem1 31861	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑦))
33		simpr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘𝑦) = 𝑢)
34	33	fveq2d 6846	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = (𝐺‘𝑢))
35		simpllr 774	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑥 = (𝐺‘𝑢))
36	34, 35	eqtr4d 2779	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐺‘(𝐹‘𝑦)) = 𝑥)
37	36	fveq2d 6846	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → (𝐹‘(𝐺‘(𝐹‘𝑦))) = (𝐹‘𝑥))
38	32, 37, 33	3eqtr3rd 2785	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑢) → 𝑢 = (𝐹‘𝑥))
39	17	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝐹 Fn 𝐴)
40		simplrr 776	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 ∈ ran 𝐹)
41		fvelrnb 6903	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢))
42	41	biimpa 477	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
43	39, 40, 42	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑢)
44	38, 43	r19.29a 3159	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑥 = (𝐺‘𝑢)) → 𝑢 = (𝐹‘𝑥))
45	8	ad4antr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑉 ∈ Poset)
46	11	ad4antr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑊 ∈ Poset)
47	2	ad4antr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝐹𝐻𝐺)
48		simplr 767	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑣 ∈ 𝐵)
49	7, 3, 4, 5, 6, 45, 46, 47, 48	mgcf1olem2 31862	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
50		simpr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘𝑣) = 𝑥)
51	50	fveq2d 6846	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑥))
52		simpllr 774	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑢 = (𝐹‘𝑥))
53	51, 52	eqtr4d 2779	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐹‘(𝐺‘𝑣)) = 𝑢)
54	53	fveq2d 6846	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑢))
55	49, 54, 50	3eqtr3rd 2785	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑥) → 𝑥 = (𝐺‘𝑢))
56	23	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝐺 Fn 𝐵)
57		simplrl 775	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 ∈ ran 𝐺)
58		fvelrnb 6903	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥))
59	58	biimpa 477	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
60	56, 57, 59	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑥)
61	55, 60	r19.29a 3159	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) ∧ 𝑢 = (𝐹‘𝑥)) → 𝑥 = (𝐺‘𝑢))
62	44, 61	impbida 799	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹)) → (𝑥 = (𝐺‘𝑢) ↔ 𝑢 = (𝐹‘𝑥)))
63	1, 22, 27, 62	f1o2d 7607	. . 3 ⊢ (𝜑 → (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)):ran 𝐺–1-1-onto→ran 𝐹)
64	16, 19	feqresmpt 6911	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) = (𝑥 ∈ ran 𝐺 ↦ (𝐹‘𝑥)))
65	64	f1oeq1d 6779	. . 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 773	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝜑)
68	19	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ran 𝐺 ⊆ 𝐴)
69		simplr 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺)
70	68, 69	sseldd 3945	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑥 ∈ 𝐴)
71	70	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ∈ 𝐴)
72		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ ran 𝐺)
73	68, 72	sseldd 3945	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → 𝑦 ∈ 𝐴)
74	73	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴)
75		simpr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦)
76	15	simprld 770	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))))
77	76	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
78	77	r19.21bi 3234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
79	78	r19.21bi 3234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
80	79	imp 407	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
81	67, 71, 74, 75, 80	syl1111anc 838	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
82	69	fvresd 6862	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
83	82	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) = (𝐹‘𝑥))
84	72	fvresd 6862	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
85	84	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑦) = (𝐹‘𝑦))
86	81, 83, 85	3brtr4d 5137	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ 𝑥 ≤ 𝑦) → ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦))
87	82, 84	breq12d 5118	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦) ↔ (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
88	87	biimpa 477	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
89	11	ad7antr 736	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑊 ∈ Poset)
90	8	ad7antr 736	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑉 ∈ Poset)
91	7, 10, 13, 2	mgcmnt2d 31858	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
92	91	ad7antr 736	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺 ∈ (𝑊Monot𝑉))
93	16	ad7antr 736	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹:𝐴⟶𝐵)
94	18	ad7antr 736	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐺:𝐵⟶𝐴)
95		simp-4r 782	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑢 ∈ 𝐵)
96	94, 95	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ∈ 𝐴)
97	93, 96	ffvelcdmd 7036	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ∈ 𝐵)
98		simplr 767	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑣 ∈ 𝐵)
99	94, 98	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) ∈ 𝐴)
100	93, 99	ffvelcdmd 7036	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) ∈ 𝐵)
101		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
102	101	ad4antr 730	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘𝑥) ≲ (𝐹‘𝑦))
103		simpllr 774	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) = 𝑥)
104	103	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘𝑥))
105		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑣) = 𝑦)
106	105	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑣)) = (𝐹‘𝑦))
107	102, 104, 106	3brtr4d 5137	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐹‘(𝐺‘𝑢)) ≲ (𝐹‘(𝐺‘𝑣)))
108	4, 3, 6, 5, 89, 90, 92, 97, 100, 107	ismntd 31844	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) ≤ (𝐺‘(𝐹‘(𝐺‘𝑣))))
109	2	ad7antr 736	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝐹𝐻𝐺)
110	7, 3, 4, 5, 6, 90, 89, 109, 95	mgcf1olem2 31862	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑢))) = (𝐺‘𝑢))
111	7, 3, 4, 5, 6, 90, 89, 109, 98	mgcf1olem2 31862	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘(𝐹‘(𝐺‘𝑣))) = (𝐺‘𝑣))
112	108, 110, 111	3brtr3d 5136	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → (𝐺‘𝑢) ≤ (𝐺‘𝑣))
113	112, 103, 105	3brtr3d 5136	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) ∧ 𝑣 ∈ 𝐵) ∧ (𝐺‘𝑣) = 𝑦) → 𝑥 ≤ 𝑦)
114	23	ad3antrrr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝐺 Fn 𝐵)
115	114	ad2antrr 724	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝐺 Fn 𝐵)
116		simp-4r 782	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑦 ∈ ran 𝐺)
117		fvelrnb 6903	. . . . . . . . . 10 ⊢ (𝐺 Fn 𝐵 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦))
118	117	biimpa 477	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
119	115, 116, 118	syl2anc 584	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → ∃𝑣 ∈ 𝐵 (𝐺‘𝑣) = 𝑦)
120	113, 119	r19.29a 3159	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ 𝑢 ∈ 𝐵) ∧ (𝐺‘𝑢) = 𝑥) → 𝑥 ≤ 𝑦)
121		simpllr 774	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ∈ ran 𝐺)
122		fvelrnb 6903	. . . . . . . . 9 ⊢ (𝐺 Fn 𝐵 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥))
123	122	biimpa 477	. . . . . . . 8 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
124	114, 121, 123	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → ∃𝑢 ∈ 𝐵 (𝐺‘𝑢) = 𝑥)
125	120, 124	r19.29a 3159	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → 𝑥 ≤ 𝑦)
126	88, 125	syldan 591	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)) → 𝑥 ≤ 𝑦)
127	86, 126	impbida 799	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
128	127	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
129	128	ralrimivva 3197	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥 ≤ 𝑦 ↔ ((𝐹 ↾ ran 𝐺)‘𝑥) ≲ ((𝐹 ↾ ran 𝐺)‘𝑦)))
130		df-isom 6505	. 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 1541 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 ⊆ wss 3910 class class class wbr 5105 ↦ cmpt 5188 ran crn 5634 ↾ cres 5635 Fn wfn 6491 ⟶wf 6492 –1-1-onto→wf1o 6495 ‘cfv 6496 Isom wiso 6497 (class class class)co 7357 Basecbs 17083 lecple 17140 Proset cproset 18182 Posetcpo 18196 Monotcmnt 31838 MGalConncmgc 31839

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-ov 7360 df-oprab 7361 df-mpo 7362 df-map 8767 df-proset 18184 df-poset 18202 df-mnt 31840 df-mgc 31841

This theorem is referenced by: nsgqusf1o 32194

W3C validator