mgcf1o

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

	Ref	Expression
Hypotheses	mgcf1o.h	$⊢ H = V MGalConn W$
	mgcf1o.a	$⊢ A = {Base}_{V}$
	mgcf1o.b	$⊢ B = {Base}_{W}$
	mgcf1o.1	$⊢ \underset{˙}{\leq} = \leq_{V}$
	mgcf1o.2	No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
	mgcf1o.v	$⊢ φ \to V \in Poset$
	mgcf1o.w	$⊢ φ \to W \in Poset$
	mgcf1o.f	$⊢ φ \to F H G$
Assertion	mgcf1o	Could not format assertion : No typesetting found for \|- ( ph -> ( F \|` ran G ) Isom .<_ , .c_ ( ran G , ran F ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		mgcf1o.h	$⊢ H = V MGalConn W$
2		mgcf1o.a	$⊢ A = {Base}_{V}$
3		mgcf1o.b	$⊢ B = {Base}_{W}$
4		mgcf1o.1	$⊢ \underset{˙}{\leq} = \leq_{V}$
5		mgcf1o.2	Could not format .c_ = ( le ` W ) : No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
6		mgcf1o.v	$⊢ φ \to V \in Poset$
7		mgcf1o.w	$⊢ φ \to W \in Poset$
8		mgcf1o.f	$⊢ φ \to F H G$
9		eqid	$⊢ (x \in ran G ⟼ F (x)) = (x \in ran G ⟼ F (x))$
10		posprs	$⊢ V \in Poset \to V \in Proset$
11	6 10	syl	$⊢ φ \to V \in Proset$
12		posprs	$⊢ W \in Poset \to W \in Proset$
13	7 12	syl	$⊢ φ \to W \in Proset$
14	2 3 4 5 1 11 13	dfmgc2	Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) : No typesetting found for \|- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) with typecode \|-
15	8 14	mpbid	Could not format ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) : No typesetting found for \|- ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) with typecode \|-
16	15	simplld	$⊢ φ \to F : A ⟶ B$
17	16	ffnd	$⊢ φ \to F Fn A$
18	15	simplrd	$⊢ φ \to G : B ⟶ A$
19	18	frnd	$⊢ φ \to ran G \subseteq A$
20	19	sselda	$⊢ (φ \land x \in ran G) \to x \in A$
21		fnfvelrn	$⊢ (F Fn A \land x \in A) \to F (x) \in ran F$
22	17 20 21	syl2an2r	$⊢ (φ \land x \in ran G) \to F (x) \in ran F$
23	18	ffnd	$⊢ φ \to G Fn B$
24	16	frnd	$⊢ φ \to ran F \subseteq B$
25	24	sselda	$⊢ (φ \land u \in ran F) \to u \in B$
26		fnfvelrn	$⊢ (G Fn B \land u \in B) \to G (u) \in ran G$
27	23 25 26	syl2an2r	$⊢ (φ \land u \in ran F) \to G (u) \in ran G$
28	6	ad4antr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to V \in Poset$
29	7	ad4antr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to W \in Poset$
30	8	ad4antr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to F H G$
31		simplr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to y \in A$
32	1 2 3 4 5 28 29 30 31	mgcf1olem1	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to F (G (F (y))) = F (y)$
33		simpr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to F (y) = u$
34	33	fveq2d	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to G (F (y)) = G (u)$
35		simpllr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to x = G (u)$
36	34 35	eqtr4d	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to G (F (y)) = x$
37	36	fveq2d	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to F (G (F (y))) = F (x)$
38	32 37 33	3eqtr3rd	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \land y \in A) \land F (y) = u) \to u = F (x)$
39	17	ad2antrr	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \to F Fn A$
40		simplrr	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \to u \in ran F$
41		fvelrnb	$⊢ F Fn A \to (u \in ran F \leftrightarrow \exists y \in A F (y) = u)$
42	41	biimpa	$⊢ (F Fn A \land u \in ran F) \to \exists y \in A F (y) = u$
43	39 40 42	syl2anc	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \to \exists y \in A F (y) = u$
44	38 43	r19.29a	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land x = G (u)) \to u = F (x)$
45	6	ad4antr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to V \in Poset$
46	7	ad4antr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to W \in Poset$
47	8	ad4antr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to F H G$
48		simplr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to v \in B$
49	1 2 3 4 5 45 46 47 48	mgcf1olem2	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to G (F (G (v))) = G (v)$
50		simpr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to G (v) = x$
51	50	fveq2d	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to F (G (v)) = F (x)$
52		simpllr	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to u = F (x)$
53	51 52	eqtr4d	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to F (G (v)) = u$
54	53	fveq2d	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to G (F (G (v))) = G (u)$
55	49 54 50	3eqtr3rd	$⊢ ((((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \land v \in B) \land G (v) = x) \to x = G (u)$
56	23	ad2antrr	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \to G Fn B$
57		simplrl	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \to x \in ran G$
58		fvelrnb	$⊢ G Fn B \to (x \in ran G \leftrightarrow \exists v \in B G (v) = x)$
59	58	biimpa	$⊢ (G Fn B \land x \in ran G) \to \exists v \in B G (v) = x$
60	56 57 59	syl2anc	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \to \exists v \in B G (v) = x$
61	55 60	r19.29a	$⊢ ((φ \land (x \in ran G \land u \in ran F)) \land u = F (x)) \to x = G (u)$
62	44 61	impbida	$⊢ (φ \land (x \in ran G \land u \in ran F)) \to (x = G (u) \leftrightarrow u = F (x))$
63	9 22 27 62	f1o2d	$⊢ φ \to (x \in ran G ⟼ F (x)) : ran G \underset{1-1 onto}{⟶} ran F$
64	16 19	feqresmpt	$⊢ φ \to {F ↾}_{ran G} = (x \in ran G ⟼ F (x))$
65	64	f1oeq1d	$⊢ φ \to (({F ↾}_{ran G}) : ran G \underset{1-1 onto}{⟶} ran F \leftrightarrow (x \in ran G ⟼ F (x)) : ran G \underset{1-1 onto}{⟶} ran F)$
66	63 65	mpbird	$⊢ φ \to ({F ↾}_{ran G}) : ran G \underset{1-1 onto}{⟶} ran F$
67		simplll	$⊢ (((φ \land x \in ran G) \land y \in ran G) \land x \underset{˙}{\leq} y) \to φ$
68	19	ad2antrr	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to ran G \subseteq A$
69		simplr	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to x \in ran G$
70	68 69	sseldd	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to x \in A$
71	70	adantr	$⊢ (((φ \land x \in ran G) \land y \in ran G) \land x \underset{˙}{\leq} y) \to x \in A$
72		simpr	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to y \in ran G$
73	68 72	sseldd	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to y \in A$
74	73	adantr	$⊢ (((φ \land x \in ran G) \land y \in ran G) \land x \underset{˙}{\leq} y) \to y \in A$
75		simpr	$⊢ (((φ \land x \in ran G) \land y \in ran G) \land x \underset{˙}{\leq} y) \to x \underset{˙}{\leq} y$
76	15	simprld	Could not format ( ph -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) : No typesetting found for \|- ( ph -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) with typecode \|-
77	76	simpld	Could not format ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for \|- ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode \|-
78	77	r19.21bi	Could not format ( ( ph /\ x e. A ) -> A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for \|- ( ( ph /\ x e. A ) -> A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode \|-
79	78	r19.21bi	Could not format ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for \|- ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode \|-
80	79	imp	Could not format ( ( ( ( ph /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) ) : No typesetting found for \|- ( ( ( ( ph /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) ) with typecode \|-
81	67 71 74 75 80	syl1111anc	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) ) with typecode \|-
82	69	fvresd	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to ({F ↾}_{ran G}) (x) = F (x)$
83	82	adantr	$⊢ (((φ \land x \in ran G) \land y \in ran G) \land x \underset{˙}{\leq} y) \to ({F ↾}_{ran G}) (x) = F (x)$
84	72	fvresd	$⊢ ((φ \land x \in ran G) \land y \in ran G) \to ({F ↾}_{ran G}) (y) = F (y)$
85	84	adantr	$⊢ (((φ \land x \in ran G) \land y \in ran G) \land x \underset{˙}{\leq} y) \to ({F ↾}_{ran G}) (y) = F (y)$
86	81 83 85	3brtr4d	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ x .<_ y ) -> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ x .<_ y ) -> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) with typecode \|-
87	82 84	breq12d	Could not format ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) -> ( ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for \|- ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) -> ( ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) ) with typecode \|-
88	87	biimpa	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) -> ( F ` x ) .c_ ( F ` y ) ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) -> ( F ` x ) .c_ ( F ` y ) ) with typecode \|-
89	7	ad7antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> W e. Poset ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> W e. Poset ) with typecode \|-
90	6	ad7antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> V e. Poset ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> V e. Poset ) with typecode \|-
91	1 11 13 8	mgcmnt2d	$⊢ φ \to G \in (W Monot V)$
92	91	ad7antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> G e. ( W Monot V ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> G e. ( W Monot V ) ) with typecode \|-
93	16	ad7antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> F : A --> B ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> F : A --> B ) with typecode \|-
94	18	ad7antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> G : B --> A ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> G : B --> A ) with typecode \|-
95		simp-4r	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> u e. B ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> u e. B ) with typecode \|-
96	94 95	ffvelcdmd	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` u ) e. A ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` u ) e. A ) with typecode \|-
97	93 96	ffvelcdmd	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` u ) ) e. B ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` u ) ) e. B ) with typecode \|-
98		simplr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> v e. B ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> v e. B ) with typecode \|-
99	94 98	ffvelcdmd	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` v ) e. A ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` v ) e. A ) with typecode \|-
100	93 99	ffvelcdmd	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` v ) ) e. B ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` v ) ) e. B ) with typecode \|-
101		simpr	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> ( F ` x ) .c_ ( F ` y ) ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> ( F ` x ) .c_ ( F ` y ) ) with typecode \|-
102	101	ad4antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` x ) .c_ ( F ` y ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` x ) .c_ ( F ` y ) ) with typecode \|-
103		simpllr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` u ) = x ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` u ) = x ) with typecode \|-
104	103	fveq2d	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` u ) ) = ( F ` x ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` u ) ) = ( F ` x ) ) with typecode \|-
105		simpr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` v ) = y ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` v ) = y ) with typecode \|-
106	105	fveq2d	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` v ) ) = ( F ` y ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` v ) ) = ( F ` y ) ) with typecode \|-
107	102 104 106	3brtr4d	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` u ) ) .c_ ( F ` ( G ` v ) ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( F ` ( G ` u ) ) .c_ ( F ` ( G ` v ) ) ) with typecode \|-
108	3 2 5 4 89 90 92 97 100 107	ismntd	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` ( F ` ( G ` u ) ) ) .<_ ( G ` ( F ` ( G ` v ) ) ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` ( F ` ( G ` u ) ) ) .<_ ( G ` ( F ` ( G ` v ) ) ) ) with typecode \|-
109	8	ad7antr	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> F H G ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> F H G ) with typecode \|-
110	1 2 3 4 5 90 89 109 95	mgcf1olem2	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` ( F ` ( G ` u ) ) ) = ( G ` u ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` ( F ` ( G ` u ) ) ) = ( G ` u ) ) with typecode \|-
111	1 2 3 4 5 90 89 109 98	mgcf1olem2	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` ( F ` ( G ` v ) ) ) = ( G ` v ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` ( F ` ( G ` v ) ) ) = ( G ` v ) ) with typecode \|-
112	108 110 111	3brtr3d	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` u ) .<_ ( G ` v ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> ( G ` u ) .<_ ( G ` v ) ) with typecode \|-
113	112 103 105	3brtr3d	Could not format ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> x .<_ y ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) /\ v e. B ) /\ ( G ` v ) = y ) -> x .<_ y ) with typecode \|-
114	23	ad3antrrr	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> G Fn B ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> G Fn B ) with typecode \|-
115	114	ad2antrr	Could not format ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> G Fn B ) : No typesetting found for \|- ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> G Fn B ) with typecode \|-
116		simp-4r	Could not format ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> y e. ran G ) : No typesetting found for \|- ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> y e. ran G ) with typecode \|-
117		fvelrnb	$⊢ G Fn B \to (y \in ran G \leftrightarrow \exists v \in B G (v) = y)$
118	117	biimpa	$⊢ (G Fn B \land y \in ran G) \to \exists v \in B G (v) = y$
119	115 116 118	syl2anc	Could not format ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> E. v e. B ( G ` v ) = y ) : No typesetting found for \|- ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> E. v e. B ( G ` v ) = y ) with typecode \|-
120	113 119	r19.29a	Could not format ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> x .<_ y ) : No typesetting found for \|- ( ( ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) /\ u e. B ) /\ ( G ` u ) = x ) -> x .<_ y ) with typecode \|-
121		simpllr	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> x e. ran G ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> x e. ran G ) with typecode \|-
122		fvelrnb	$⊢ G Fn B \to (x \in ran G \leftrightarrow \exists u \in B G (u) = x)$
123	122	biimpa	$⊢ (G Fn B \land x \in ran G) \to \exists u \in B G (u) = x$
124	114 121 123	syl2anc	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> E. u e. B ( G ` u ) = x ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> E. u e. B ( G ` u ) = x ) with typecode \|-
125	120 124	r19.29a	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> x .<_ y ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( F ` x ) .c_ ( F ` y ) ) -> x .<_ y ) with typecode \|-
126	88 125	syldan	Could not format ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) -> x .<_ y ) : No typesetting found for \|- ( ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) /\ ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) -> x .<_ y ) with typecode \|-
127	86 126	impbida	Could not format ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) -> ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) : No typesetting found for \|- ( ( ( ph /\ x e. ran G ) /\ y e. ran G ) -> ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) with typecode \|-
128	127	anasss	Could not format ( ( ph /\ ( x e. ran G /\ y e. ran G ) ) -> ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) : No typesetting found for \|- ( ( ph /\ ( x e. ran G /\ y e. ran G ) ) -> ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) with typecode \|-
129	128	ralrimivva	Could not format ( ph -> A. x e. ran G A. y e. ran G ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) : No typesetting found for \|- ( ph -> A. x e. ran G A. y e. ran G ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) with typecode \|-
130		df-isom	Could not format ( ( F \|` ran G ) Isom .<_ , .c_ ( ran G , ran F ) <-> ( ( F \|` ran G ) : ran G -1-1-onto-> ran F /\ A. x e. ran G A. y e. ran G ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) ) : No typesetting found for \|- ( ( F \|` ran G ) Isom .<_ , .c_ ( ran G , ran F ) <-> ( ( F \|` ran G ) : ran G -1-1-onto-> ran F /\ A. x e. ran G A. y e. ran G ( x .<_ y <-> ( ( F \|` ran G ) ` x ) .c_ ( ( F \|` ran G ) ` y ) ) ) ) with typecode \|-
131	66 129 130	sylanbrc	Could not format ( ph -> ( F \|` ran G ) Isom .<_ , .c_ ( ran G , ran F ) ) : No typesetting found for \|- ( ph -> ( F \|` ran G ) Isom .<_ , .c_ ( ran G , ran F ) ) with typecode \|-

Metamath Proof Explorer

Theorem mgcf1o

Proof