Theorem dfmgc2lem

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

	Ref	Expression
Hypotheses	mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
	mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
	mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mgcoval.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
	mgcval.1	$$⊢H=V\mathrm{MGalConn}W$$
	mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
	dfmgc2lem.1	$$⊢\phi \to F:A⟶B$$
	dfmgc2lem.2	$$⊢\phi \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	$$⊢\left(\phi \wedge x\in A\right)\to x\underset{\dot{}}{\le }G\left(F\left(x\right)\right)$$
	dfmgc2lem.6	No typesetting found for |- ( ( ph /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u ) with typecode |-
Assertion	dfmgc2lem	$$⊢\phi \to FHG$$

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
2		mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5		mgcval.1	$$⊢H=V\mathrm{MGalConn}W$$
6		mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
7		mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
8		dfmgc2lem.1	$$⊢\phi \to F:A⟶B$$
9		dfmgc2lem.2	$$⊢\phi \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	$$⊢\left(\phi \wedge x\in A\right)\to x\underset{\dot{}}{\le }G\left(F\left(x\right)\right)$$
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	$$⊢\phi \to \left(F:A⟶B\wedge G:B⟶A\right)$$
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	$$⊢\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\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	$$⊢\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\to G:B⟶A$$
23		simpr	$$⊢\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\to w\in B$$
24	22 23	ffvelcdmd	$$⊢\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\to G\left(w\right)\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	$$⊢\phi \to \forall x\in Ax\underset{\dot{}}{\le }G\left(F\left(x\right)\right)$$
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\left(z\right)\to G\left(u\right)=G\left(F\left(z\right)\right)$$
37	36	breq1d	$$⊢u=F\left(z\right)\to \left(G\left(u\right)\underset{\dot{}}{\le }G\left(v\right)\leftrightarrow G\left(F\left(z\right)\right)\underset{\dot{}}{\le }G\left(v\right)\right)$$
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\left(v\right)=G\left(w\right)$$
41	40	breq2d	$$⊢v=w\to \left(G\left(F\left(z\right)\right)\underset{\dot{}}{\le }G\left(v\right)\leftrightarrow G\left(F\left(z\right)\right)\underset{\dot{}}{\le }G\left(w\right)\right)$$
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	$$⊢\left(\phi \wedge z\in A\right)\to F\left(z\right)\in B$$
44	43	adantr	$$⊢\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\to F\left(z\right)\in B$$
45		eqidd	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge u=F\left(z\right)\right)\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	$$⊢\left(V\in \mathrm{Proset}\wedge \left(z\in A\wedge G\left(F\left(z\right)\right)\in A\wedge G\left(w\right)\in A\right)\wedge \left(z\underset{\dot{}}{\le }G\left(F\left(z\right)\right)\wedge G\left(F\left(z\right)\right)\underset{\dot{}}{\le }G\left(w\right)\right)\right)\to z\underset{\dot{}}{\le }G\left(w\right)$$
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	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\to W\in \mathrm{Proset}$$
52	43	ad2antrr	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\to F\left(z\right)\in B$$
53	8	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\to F:A⟶B$$
54	24	adantr	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\to G\left(w\right)\in A$$
55	53 54	ffvelcdmd	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\to F\left(G\left(w\right)\right)\in B$$
56		simplr	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\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 \left(x\underset{\dot{}}{\le }y\leftrightarrow z\underset{\dot{}}{\le }y\right)$$
59		fveq2	$$⊢x=z\to F\left(x\right)=F\left(z\right)$$
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\left(w\right)\to \left(z\underset{\dot{}}{\le }y\leftrightarrow z\underset{\dot{}}{\le }G\left(w\right)\right)$$
63		fveq2	$$⊢y=G\left(w\right)\to F\left(y\right)=F\left(G\left(w\right)\right)$$
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	$$⊢\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge x=z\right)\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	$$⊢\left(\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\wedge u=w\right)\to u=w$$
73	72	fveq2d	$$⊢\left(\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\wedge u=w\right)\to G\left(u\right)=G\left(w\right)$$
74	73	fveq2d	$$⊢\left(\left(\left(\left(\phi \wedge z\in A\right)\wedge w\in B\right)\wedge z\underset{\dot{}}{\le }G\left(w\right)\right)\wedge u=w\right)\to F\left(G\left(u\right)\right)=F\left(G\left(w\right)\right)$$
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	$$⊢\phi \to FHG$$