dfmgc2lem

Description: Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024)

	Ref	Expression
Hypotheses	mgcoval.1	$⊢ A = {Base}_{V}$
	mgcoval.2	$⊢ B = {Base}_{W}$
	mgcoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
	mgcoval.4	No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
	mgcval.1	$⊢ H = V MGalConn W$
	mgcval.2	$⊢ φ \to V \in Proset$
	mgcval.3	$⊢ φ \to W \in Proset$
	dfmgc2lem.1	$⊢ φ \to F : A ⟶ B$
	dfmgc2lem.2	$⊢ φ \to G : B ⟶ A$
	dfmgc2lem.3	No typesetting found for \|- ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode \|-
	dfmgc2lem.4	No typesetting found for \|- ( ph -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode \|-
	dfmgc2lem.5	$⊢ (φ \land x \in A) \to x \underset{˙}{\leq} G (F (x))$
	dfmgc2lem.6	No typesetting found for \|- ( ( ph /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u ) with typecode \|-
Assertion	dfmgc2lem	$⊢ φ \to F H G$

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$⊢ A = {Base}_{V}$
2		mgcoval.2	$⊢ B = {Base}_{W}$
3		mgcoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
5		mgcval.1	$⊢ H = V MGalConn W$
6		mgcval.2	$⊢ φ \to V \in Proset$
7		mgcval.3	$⊢ φ \to W \in Proset$
8		dfmgc2lem.1	$⊢ φ \to F : A ⟶ B$
9		dfmgc2lem.2	$⊢ φ \to G : B ⟶ A$
10		dfmgc2lem.3	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 \|-
11		dfmgc2lem.4	Could not format ( ph -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) : No typesetting found for \|- ( ph -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode \|-
12		dfmgc2lem.5	$⊢ (φ \land x \in A) \to x \underset{˙}{\leq} G (F (x))$
13		dfmgc2lem.6	Could not format ( ( ph /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u ) : No typesetting found for \|- ( ( ph /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u ) with typecode \|-
14	8 9	jca	$⊢ φ \to (F : A ⟶ B \land G : B ⟶ A)$
15	6	ad3antrrr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> V e. Proset ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> V e. Proset ) with typecode \|-
16		simplr	$⊢ ((φ \land z \in A) \land w \in B) \to z \in A$
17	16	adantr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z e. A ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z e. A ) with typecode \|-
18	9	ad3antrrr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> G : B --> A ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> G : B --> A ) with typecode \|-
19	8	ad3antrrr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> F : A --> B ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> F : A --> B ) with typecode \|-
20	19 17	ffvelcdmd	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( F ` z ) e. B ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( F ` z ) e. B ) with typecode \|-
21	18 20	ffvelcdmd	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` ( F ` z ) ) e. A ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` ( F ` z ) ) e. A ) with typecode \|-
22	9	ad2antrr	$⊢ ((φ \land z \in A) \land w \in B) \to G : B ⟶ A$
23		simpr	$⊢ ((φ \land z \in A) \land w \in B) \to w \in B$
24	22 23	ffvelcdmd	$⊢ ((φ \land z \in A) \land w \in B) \to G (w) \in A$
25	24	adantr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` w ) e. A ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` w ) e. A ) with typecode \|-
26	12	ralrimiva	$⊢ φ \to \forall x \in A x \underset{˙}{\leq} G (F (x))$
27	26	ad3antrrr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) ) with typecode \|-
28		simpr	Could not format ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> x = z ) : No typesetting found for \|- ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> x = z ) with typecode \|-
29	28	fveq2d	Could not format ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( F ` x ) = ( F ` z ) ) : No typesetting found for \|- ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( F ` x ) = ( F ` z ) ) with typecode \|-
30	29	fveq2d	Could not format ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( G ` ( F ` x ) ) = ( G ` ( F ` z ) ) ) : No typesetting found for \|- ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( G ` ( F ` x ) ) = ( G ` ( F ` z ) ) ) with typecode \|-
31	28 30	breq12d	Could not format ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( x .<_ ( G ` ( F ` x ) ) <-> z .<_ ( G ` ( F ` z ) ) ) ) : No typesetting found for \|- ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( x .<_ ( G ` ( F ` x ) ) <-> z .<_ ( G ` ( F ` z ) ) ) ) with typecode \|-
32	17 31	rspcdv	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( A. x e. A x .<_ ( G ` ( F ` x ) ) -> z .<_ ( G ` ( F ` z ) ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( A. x e. A x .<_ ( G ` ( F ` x ) ) -> z .<_ ( G ` ( F ` z ) ) ) ) with typecode \|-
33	27 32	mpd	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z .<_ ( G ` ( F ` z ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z .<_ ( G ` ( F ` z ) ) ) with typecode \|-
34	11	ad2antrr	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode \|-
35		breq1	Could not format ( u = ( F ` z ) -> ( u .c_ v <-> ( F ` z ) .c_ v ) ) : No typesetting found for \|- ( u = ( F ` z ) -> ( u .c_ v <-> ( F ` z ) .c_ v ) ) with typecode \|-
36		fveq2	$⊢ u = F (z) \to G (u) = G (F (z))$
37	36	breq1d	$⊢ u = F (z) \to (G (u) \underset{˙}{\leq} G (v) \leftrightarrow G (F (z)) \underset{˙}{\leq} G (v))$
38	35 37	imbi12d	Could not format ( u = ( F ` z ) -> ( ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> ( ( F ` z ) .c_ v -> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) ) ) : No typesetting found for \|- ( u = ( F ` z ) -> ( ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> ( ( F ` z ) .c_ v -> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) ) ) with typecode \|-
39		breq2	Could not format ( v = w -> ( ( F ` z ) .c_ v <-> ( F ` z ) .c_ w ) ) : No typesetting found for \|- ( v = w -> ( ( F ` z ) .c_ v <-> ( F ` z ) .c_ w ) ) with typecode \|-
40		fveq2	$⊢ v = w \to G (v) = G (w)$
41	40	breq2d	$⊢ v = w \to (G (F (z)) \underset{˙}{\leq} G (v) \leftrightarrow G (F (z)) \underset{˙}{\leq} G (w))$
42	39 41	imbi12d	Could not format ( v = w -> ( ( ( F ` z ) .c_ v -> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) <-> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) ) : No typesetting found for \|- ( v = w -> ( ( ( F ` z ) .c_ v -> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) <-> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) ) with typecode \|-
43	8	ffvelcdmda	$⊢ (φ \land z \in A) \to F (z) \in B$
44	43	adantr	$⊢ ((φ \land z \in A) \land w \in B) \to F (z) \in B$
45		eqidd	$⊢ (((φ \land z \in A) \land w \in B) \land u = F (z)) \to B = B$
46	38 42 44 45 23	rspc2vd	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) -> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) -> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) ) with typecode \|-
47	34 46	mpd	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) with typecode \|-
48	47	imp	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) with typecode \|-
49	1 3	prstr	$⊢ (V \in Proset \land (z \in A \land G (F (z)) \in A \land G (w) \in A) \land (z \underset{˙}{\leq} G (F (z)) \land G (F (z)) \underset{˙}{\leq} G (w))) \to z \underset{˙}{\leq} G (w)$
50	15 17 21 25 33 48 49	syl132anc	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z .<_ ( G ` w ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z .<_ ( G ` w ) ) with typecode \|-
51	7	ad3antrrr	$⊢ (((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \to W \in Proset$
52	43	ad2antrr	$⊢ (((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \to F (z) \in B$
53	8	ad3antrrr	$⊢ (((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \to F : A ⟶ B$
54	24	adantr	$⊢ (((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \to G (w) \in A$
55	53 54	ffvelcdmd	$⊢ (((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \to F (G (w)) \in B$
56		simplr	$⊢ (((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \to w \in B$
57	10	ad2antrr	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode \|-
58		breq1	$⊢ x = z \to (x \underset{˙}{\leq} y \leftrightarrow z \underset{˙}{\leq} y)$
59		fveq2	$⊢ x = z \to F (x) = F (z)$
60	59	breq1d	Could not format ( x = z -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` z ) .c_ ( F ` y ) ) ) : No typesetting found for \|- ( x = z -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` z ) .c_ ( F ` y ) ) ) with typecode \|-
61	58 60	imbi12d	Could not format ( x = z -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( z .<_ y -> ( F ` z ) .c_ ( F ` y ) ) ) ) : No typesetting found for \|- ( x = z -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( z .<_ y -> ( F ` z ) .c_ ( F ` y ) ) ) ) with typecode \|-
62		breq2	$⊢ y = G (w) \to (z \underset{˙}{\leq} y \leftrightarrow z \underset{˙}{\leq} G (w))$
63		fveq2	$⊢ y = G (w) \to F (y) = F (G (w))$
64	63	breq2d	Could not format ( y = ( G ` w ) -> ( ( F ` z ) .c_ ( F ` y ) <-> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) : No typesetting found for \|- ( y = ( G ` w ) -> ( ( F ` z ) .c_ ( F ` y ) <-> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) with typecode \|-
65	62 64	imbi12d	Could not format ( y = ( G ` w ) -> ( ( z .<_ y -> ( F ` z ) .c_ ( F ` y ) ) <-> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) ) : No typesetting found for \|- ( y = ( G ` w ) -> ( ( z .<_ y -> ( F ` z ) .c_ ( F ` y ) ) <-> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) ) with typecode \|-
66		eqidd	$⊢ (((φ \land z \in A) \land w \in B) \land x = z) \to A = A$
67	61 65 16 66 24	rspc2vd	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) -> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) -> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) ) with typecode \|-
68	57 67	mpd	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) with typecode \|-
69	68	imp	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) with typecode \|-
70	13	ralrimiva	Could not format ( ph -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) : No typesetting found for \|- ( ph -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) with typecode \|-
71	70	ad3antrrr	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) with typecode \|-
72		simpr	$⊢ ((((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \land u = w) \to u = w$
73	72	fveq2d	$⊢ ((((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \land u = w) \to G (u) = G (w)$
74	73	fveq2d	$⊢ ((((φ \land z \in A) \land w \in B) \land z \underset{˙}{\leq} G (w)) \land u = w) \to F (G (u)) = F (G (w))$
75	74 72	breq12d	Could not format ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) /\ u = w ) -> ( ( F ` ( G ` u ) ) .c_ u <-> ( F ` ( G ` w ) ) .c_ w ) ) : No typesetting found for \|- ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) /\ u = w ) -> ( ( F ` ( G ` u ) ) .c_ u <-> ( F ` ( G ` w ) ) .c_ w ) ) with typecode \|-
76	56 75	rspcdv	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( A. u e. B ( F ` ( G ` u ) ) .c_ u -> ( F ` ( G ` w ) ) .c_ w ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( A. u e. B ( F ` ( G ` u ) ) .c_ u -> ( F ` ( G ` w ) ) .c_ w ) ) with typecode \|-
77	71 76	mpd	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` ( G ` w ) ) .c_ w ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` ( G ` w ) ) .c_ w ) with typecode \|-
78	2 4	prstr	Could not format ( ( W e. Proset /\ ( ( F ` z ) e. B /\ ( F ` ( G ` w ) ) e. B /\ w e. B ) /\ ( ( F ` z ) .c_ ( F ` ( G ` w ) ) /\ ( F ` ( G ` w ) ) .c_ w ) ) -> ( F ` z ) .c_ w ) : No typesetting found for \|- ( ( W e. Proset /\ ( ( F ` z ) e. B /\ ( F ` ( G ` w ) ) e. B /\ w e. B ) /\ ( ( F ` z ) .c_ ( F ` ( G ` w ) ) /\ ( F ` ( G ` w ) ) .c_ w ) ) -> ( F ` z ) .c_ w ) with typecode \|-
79	51 52 55 56 69 77 78	syl132anc	Could not format ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) .c_ w ) : No typesetting found for \|- ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) .c_ w ) with typecode \|-
80	50 79	impbida	Could not format ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) with typecode \|-
81	80	anasss	Could not format ( ( ph /\ ( z e. A /\ w e. B ) ) -> ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) : No typesetting found for \|- ( ( ph /\ ( z e. A /\ w e. B ) ) -> ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) with typecode \|-
82	81	ralrimivva	Could not format ( ph -> A. z e. A A. w e. B ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) : No typesetting found for \|- ( ph -> A. z e. A A. w e. B ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) with typecode \|-
83	1 2 3 4 5 6 7	mgcval	Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. z e. A A. w e. B ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) ) ) : No typesetting found for \|- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. z e. A A. w e. B ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) ) ) with typecode \|-
84	14 82 83	mpbir2and	$⊢ φ \to F H G$

Metamath Proof Explorer

Theorem dfmgc2lem

Proof