Theorem wemapwe 8138

Description: Construct lexicographic order on a function space based on a reverse well-ordering of the indexes and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by AV, 3-Jul-2019.)

Hypotheses

Ref	Expression
wemapwe.t	|- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) }
wemapwe.u	|- U = { x e. ( B ^m A ) | x finSupp Z }
wemapwe.2	|- ( ph -> R We A )
wemapwe.3	|- ( ph -> S We B )
wemapwe.4	|- ( ph -> B =/= (/) )
wemapwe.5	|- F = OrdIso ( R , A )
wemapwe.6	|- G = OrdIso ( S , B )
wemapwe.7	|- Z = ( G ` (/) )

Assertion

Ref	Expression
wemapwe	|- ( ph -> T We U )

Distinct variable groups:   x, w, y, z, A   x, B, y   w, F, x, y, z   x, G, y   ph, x, y   w, R, z   z, S   x, U, y   x, Z

Allowed substitution hints:   ph( z, w)   B( z, w)   R( x, y)   S( x, y, w)   T( x, y, z, w)   U( z, w)   G( z, w)   Z( y, z, w)

Proof of Theorem wemapwe

Dummy variables a b c d f are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wemapwe.u	. . . . . . . . 9 |- U = { x e. ( B ^m A ) | x finSupp Z }
2		eqid 2467	. . . . . . . . 9 |- { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } = { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) }
3		eqid 2467	. . . . . . . . 9 |- ( `' G ` Z ) = ( `' G ` Z )
4		simprr 756	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> A e. _V )
5		wemapwe.2	. . . . . . . . . . . 12 |- ( ph -> R We A )
6	5	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> R We A )
7		wemapwe.5	. . . . . . . . . . . 12 |- F = OrdIso ( R , A )
8	7	oiiso 7961	. . . . . . . . . . 11 |- ( ( A e. _V /\ R We A ) -> F Isom _E , R ( dom F , A ) )
9	4, 6, 8	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F Isom _E , R ( dom F , A ) )
10		isof1o 6208	. . . . . . . . . 10 |- ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A )
11	9, 10	syl 16	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F : dom F -1-1-onto-> A )
12		simprl 755	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B e. _V )
13		wemapwe.3	. . . . . . . . . . . 12 |- ( ph -> S We B )
14	13	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> S We B )
15		wemapwe.6	. . . . . . . . . . . 12 |- G = OrdIso ( S , B )
16	15	oiiso 7961	. . . . . . . . . . 11 |- ( ( B e. _V /\ S We B ) -> G Isom _E , S ( dom G , B ) )
17	12, 14, 16	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G Isom _E , S ( dom G , B ) )
18		isof1o 6208	. . . . . . . . . 10 |- ( G Isom _E , S ( dom G , B ) -> G : dom G -1-1-onto-> B )
19		f1ocnv 5827	. . . . . . . . . 10 |- ( G : dom G -1-1-onto-> B -> `' G : B -1-1-onto-> dom G )
20	17, 18, 19	3syl 20	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> `' G : B -1-1-onto-> dom G )
21	7	oiexg 7959	. . . . . . . . . . 11 |- ( A e. _V -> F e. _V )
22	21	ad2antll 728	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F e. _V )
23		dmexg 6715	. . . . . . . . . 10 |- ( F e. _V -> dom F e. _V )
24	22, 23	syl 16	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. _V )
25	15	oiexg 7959	. . . . . . . . . . 11 |- ( B e. _V -> G e. _V )
26	25	ad2antrl 727	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G e. _V )
27		dmexg 6715	. . . . . . . . . 10 |- ( G e. _V -> dom G e. _V )
28	26, 27	syl 16	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. _V )
29		wemapwe.7	. . . . . . . . . 10 |- Z = ( G ` (/) )
30	17, 18	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G : dom G -1-1-onto-> B )
31		f1ofo 5822	. . . . . . . . . . . . . . 15 |- ( G : dom G -1-1-onto-> B -> G : dom G -onto-> B )
32		forn 5797	. . . . . . . . . . . . . . 15 |- ( G : dom G -onto-> B -> ran G = B )
33	30, 31, 32	3syl 20	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G = B )
34		wemapwe.4	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= (/) )
35	34	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B =/= (/) )
36	33, 35	eqnetrd 2760	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G =/= (/) )
37		dm0rn0 5218	. . . . . . . . . . . . . 14 |- ( dom G = (/) <-> ran G = (/) )
38	37	necon3bii 2735	. . . . . . . . . . . . 13 |- ( dom G =/= (/) <-> ran G =/= (/) )
39	36, 38	sylibr 212	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G =/= (/) )
40	15	oicl 7953	. . . . . . . . . . . . 13 |- Ord dom G
41		ord0eln0 4932	. . . . . . . . . . . . 13 |- ( Ord dom G -> ( (/) e. dom G <-> dom G =/= (/) ) )
42	40, 41	ax-mp 5	. . . . . . . . . . . 12 |- ( (/) e. dom G <-> dom G =/= (/) )
43	39, 42	sylibr 212	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> (/) e. dom G )
44	15	oif 7954	. . . . . . . . . . . 12 |- G : dom G --> B
45	44	ffvelrni 6019	. . . . . . . . . . 11 |- ( (/) e. dom G -> ( G ` (/) ) e. B )
46	43, 45	syl 16	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( G ` (/) ) e. B )
47	29, 46	syl5eqel 2559	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> Z e. B )
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 7866	. . . . . . . 8 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } )
49		eqid 2467	. . . . . . . . . . 11 |- { x e. ( dom G ^m dom F ) | x finSupp (/) } = { x e. ( dom G ^m dom F ) | x finSupp (/) }
50	15	oion 7960	. . . . . . . . . . . 12 |- ( B e. _V -> dom G e. On )
51	50	ad2antrl 727	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. On )
52	7	oion 7960	. . . . . . . . . . . 12 |- ( A e. _V -> dom F e. On )
53	52	ad2antll 728	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. On )
54	49, 51, 53	cantnfdm 8080	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom ( dom G CNF dom F ) = { x e. ( dom G ^m dom F ) | x finSupp (/) } )
55	29	fveq2i 5868	. . . . . . . . . . . . 13 |- ( `' G ` Z ) = ( `' G ` ( G ` (/) ) )
56		f1ocnvfv1 6169	. . . . . . . . . . . . . 14 |- ( ( G : dom G -1-1-onto-> B /\ (/) e. dom G ) -> ( `' G ` ( G ` (/) ) ) = (/) )
57	30, 43, 56	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` ( G ` (/) ) ) = (/) )
58	55, 57	syl5eq 2520	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` Z ) = (/) )
59	58	breq2d 4459	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( x finSupp ( `' G ` Z ) <-> x finSupp (/) ) )
60	59	rabbidv 3105	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } = { x e. ( dom G ^m dom F ) | x finSupp (/) } )
61	54, 60	eqtr4d 2511	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom ( dom G CNF dom F ) = { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } )
62		f1oeq3 5808	. . . . . . . . 9 |- ( dom ( dom G CNF dom F ) = { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) <-> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } ) )
63	61, 62	syl 16	. . . . . . . 8 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) <-> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } ) )
64	48, 63	mpbird 232	. . . . . . 7 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) )
65		eqid 2467	. . . . . . . . 9 |- dom ( dom G CNF dom F ) = dom ( dom G CNF dom F )
66		eqid 2467	. . . . . . . . 9 |- { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } = { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) }
67	65, 51, 53, 66	oemapwe 8112	. . . . . . . 8 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } We dom ( dom G CNF dom F ) /\ dom OrdIso ( { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } , dom ( dom G CNF dom F ) ) = ( dom G ^o dom F ) ) )
68	67	simpld 459	. . . . . . 7 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } We dom ( dom G CNF dom F ) )
69		eqid 2467	. . . . . . . 8 |- { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } = { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) }
70	69	f1owe 6236	. . . . . . 7 |- ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) -> ( { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } We dom ( dom G CNF dom F ) -> { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } We U ) )
71	64, 68, 70	sylc 60	. . . . . 6 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } We U )
72		weinxp 5066	. . . . . 6 |- ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } We U <-> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U )
73	71, 72	sylib 196	. . . . 5 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U )
74	11	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F : dom F -1-1-onto-> A )
75		f1ofn 5816	. . . . . . . . . . . 12 |- ( F : dom F -1-1-onto-> A -> F Fn dom F )
76		fveq2 5865	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
77		fveq2 5865	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
78	76, 77	breq12d 4460	. . . . . . . . . . . . . 14 |- ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
79		breq1 4450	. . . . . . . . . . . . . . . 16 |- ( z = ( F ` c ) -> ( z R w <-> ( F ` c ) R w ) )
80	79	imbi1d 317	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( ( z R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
81	80	ralbidv 2903	. . . . . . . . . . . . . 14 |- ( z = ( F ` c ) -> ( A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
82	78, 81	anbi12d 710	. . . . . . . . . . . . 13 |- ( z = ( F ` c ) -> ( ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
83	82	rexrn 6022	. . . . . . . . . . . 12 |- ( F Fn dom F -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
84	74, 75, 83	3syl 20	. . . . . . . . . . 11 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
85		f1ofo 5822	. . . . . . . . . . . . 13 |- ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
86		forn 5797	. . . . . . . . . . . . 13 |- ( F : dom F -onto-> A -> ran F = A )
87	74, 85, 86	3syl 20	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ran F = A )
88	87	rexeqdv 3065	. . . . . . . . . . 11 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) ) )
89	26	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> G e. _V )
90		cnvexg 6730	. . . . . . . . . . . . . . 15 |- ( G e. _V -> `' G e. _V )
91	89, 90	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> `' G e. _V )
92		vex 3116	. . . . . . . . . . . . . . 15 |- x e. _V
93	22	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F e. _V )
94		coexg 6735	. . . . . . . . . . . . . . 15 |- ( ( x e. _V /\ F e. _V ) -> ( x o. F ) e. _V )
95	92, 93, 94	sylancr 663	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( x o. F ) e. _V )
96		coexg 6735	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( x o. F ) e. _V ) -> ( `' G o. ( x o. F ) ) e. _V )
97	91, 95, 96	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( x o. F ) ) e. _V )
98		vex 3116	. . . . . . . . . . . . . . 15 |- y e. _V
99		coexg 6735	. . . . . . . . . . . . . . 15 |- ( ( y e. _V /\ F e. _V ) -> ( y o. F ) e. _V )
100	98, 93, 99	sylancr 663	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( y o. F ) e. _V )
101		coexg 6735	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( y o. F ) e. _V ) -> ( `' G o. ( y o. F ) ) e. _V )
102	91, 100, 101	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( y o. F ) ) e. _V )
103		fveq1 5864	. . . . . . . . . . . . . . . . 17 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
104		fveq1 5864	. . . . . . . . . . . . . . . . 17 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
105		eleq12 2543	. . . . . . . . . . . . . . . . 17 |- ( ( ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) /\ ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) ) -> ( ( a ` c ) e. ( b ` c ) <-> ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) ) )
106	103, 104, 105	syl2an 477	. . . . . . . . . . . . . . . 16 |- ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( a ` c ) e. ( b ` c ) <-> ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) ) )
107		fveq1 5864	. . . . . . . . . . . . . . . . . . 19 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
108		fveq1 5864	. . . . . . . . . . . . . . . . . . 19 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
109	107, 108	eqeqan12d 2490	. . . . . . . . . . . . . . . . . 18 |- ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( a ` d ) = ( b ` d ) <-> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) )
110	109	imbi2d 316	. . . . . . . . . . . . . . . . 17 |- ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( c e. d -> ( a ` d ) = ( b ` d ) ) <-> ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) )
111	110	ralbidv 2903	. . . . . . . . . . . . . . . 16 |- ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) <-> A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) )
112	106, 111	anbi12d 710	. . . . . . . . . . . . . . 15 |- ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) <-> ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
113	112	rexbidv 2973	. . . . . . . . . . . . . 14 |- ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
114	113, 66	brabga 4761	. . . . . . . . . . . . 13 |- ( ( ( `' G o. ( x o. F ) ) e. _V /\ ( `' G o. ( y o. F ) ) e. _V ) -> ( ( `' G o. ( x o. F ) ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( `' G o. ( y o. F ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
115	97, 102, 114	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( `' G o. ( x o. F ) ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( `' G o. ( y o. F ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
116		simprl 755	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. U )
117		coeq1 5159	. . . . . . . . . . . . . . . 16 |- ( f = x -> ( f o. F ) = ( x o. F ) )
118	117	coeq2d 5164	. . . . . . . . . . . . . . 15 |- ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
119		eqid 2467	. . . . . . . . . . . . . . 15 |- ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
120	118, 119	fvmptg 5947	. . . . . . . . . . . . . 14 |- ( ( x e. U /\ ( `' G o. ( x o. F ) ) e. _V ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) = ( `' G o. ( x o. F ) ) )
121	116, 97, 120	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) = ( `' G o. ( x o. F ) ) )
122		simprr 756	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
123		coeq1 5159	. . . . . . . . . . . . . . . 16 |- ( f = y -> ( f o. F ) = ( y o. F ) )
124	123	coeq2d 5164	. . . . . . . . . . . . . . 15 |- ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
125	124, 119	fvmptg 5947	. . . . . . . . . . . . . 14 |- ( ( y e. U /\ ( `' G o. ( y o. F ) ) e. _V ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) = ( `' G o. ( y o. F ) ) )
126	122, 102, 125	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) = ( `' G o. ( y o. F ) ) )
127	121, 126	breq12d 4460	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) <-> ( `' G o. ( x o. F ) ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( `' G o. ( y o. F ) ) ) )
128	17	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> G Isom _E , S ( dom G , B ) )
129		isocnv 6213	. . . . . . . . . . . . . . . . . 18 |- ( G Isom _E , S ( dom G , B ) -> `' G Isom S , _E ( B , dom G ) )
130	128, 129	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> `' G Isom S , _E ( B , dom G ) )
131		ssrab2 3585	. . . . . . . . . . . . . . . . . . . . 21 |- { x e. ( B ^m A ) | x finSupp Z } C_ ( B ^m A )
132	1, 131	eqsstri 3534	. . . . . . . . . . . . . . . . . . . 20 |- U C_ ( B ^m A )
133	132, 116	sseldi 3502	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
134		elmapi 7440	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( B ^m A ) -> x : A --> B )
135	133, 134	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x : A --> B )
136	7	oif 7954	. . . . . . . . . . . . . . . . . . 19 |- F : dom F --> A
137	136	ffvelrni 6019	. . . . . . . . . . . . . . . . . 18 |- ( c e. dom F -> ( F ` c ) e. A )
138		ffvelrn 6018	. . . . . . . . . . . . . . . . . 18 |- ( ( x : A --> B /\ ( F ` c ) e. A ) -> ( x ` ( F ` c ) ) e. B )
139	135, 137, 138	syl2an 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( x ` ( F ` c ) ) e. B )
140	132, 122	sseldi 3502	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
141		elmapi 7440	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( B ^m A ) -> y : A --> B )
142	140, 141	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y : A --> B )
143		ffvelrn 6018	. . . . . . . . . . . . . . . . . 18 |- ( ( y : A --> B /\ ( F ` c ) e. A ) -> ( y ` ( F ` c ) ) e. B )
144	142, 137, 143	syl2an 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( y ` ( F ` c ) ) e. B )
145		isorel 6209	. . . . . . . . . . . . . . . . 17 |- ( ( `' G Isom S , _E ( B , dom G ) /\ ( ( x ` ( F ` c ) ) e. B /\ ( y ` ( F ` c ) ) e. B ) ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) ) )
146	130, 139, 144, 145	syl12anc 1226	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) ) )
147		fvex 5875	. . . . . . . . . . . . . . . . 17 |- ( `' G ` ( y ` ( F ` c ) ) ) e. _V
148	147	epelc 4793	. . . . . . . . . . . . . . . 16 |- ( ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) )
149	146, 148	syl6bb 261	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) ) )
150	135	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> x : A --> B )
151		fco 5740	. . . . . . . . . . . . . . . . . . 19 |- ( ( x : A --> B /\ F : dom F --> A ) -> ( x o. F ) : dom F --> B )
152	150, 136, 151	sylancl 662	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( x o. F ) : dom F --> B )
153		fvco3 5943	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x o. F ) : dom F --> B /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( ( x o. F ) ` c ) ) )
154	152, 153	sylancom 667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( ( x o. F ) ` c ) ) )
155		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> c e. dom F )
156		fvco3 5943	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
157	136, 155, 156	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
158	157	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( `' G ` ( ( x o. F ) ` c ) ) = ( `' G ` ( x ` ( F ` c ) ) ) )
159	154, 158	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( x ` ( F ` c ) ) ) )
160	142	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> y : A --> B )
161		fco 5740	. . . . . . . . . . . . . . . . . . 19 |- ( ( y : A --> B /\ F : dom F --> A ) -> ( y o. F ) : dom F --> B )
162	160, 136, 161	sylancl 662	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( y o. F ) : dom F --> B )
163		fvco3 5943	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y o. F ) : dom F --> B /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( ( y o. F ) ` c ) ) )
164	162, 163	sylancom 667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( ( y o. F ) ` c ) ) )
165		fvco3 5943	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
166	136, 155, 165	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
167	166	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( `' G ` ( ( y o. F ) ` c ) ) = ( `' G ` ( y ` ( F ` c ) ) ) )
168	164, 167	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( y ` ( F ` c ) ) ) )
169	159, 168	eleq12d 2549	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) ) )
170	149, 169	bitr4d 256	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) ) )
171	87	raleqdv 3064	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
172		breq2 4451	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
173		fveq2 5865	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
174		fveq2 5865	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
175	173, 174	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( x ` w ) = ( y ` w ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
176	172, 175	imbi12d 320	. . . . . . . . . . . . . . . . . . 19 |- ( w = ( F ` d ) -> ( ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
177	176	ralrn 6023	. . . . . . . . . . . . . . . . . 18 |- ( F Fn dom F -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
178	74, 75, 177	3syl 20	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
179	171, 178	bitr3d 255	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
180	179	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
181		epel 4794	. . . . . . . . . . . . . . . . . . 19 |- ( c _E d <-> c e. d )
182	9	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> F Isom _E , R ( dom F , A ) )
183		isorel 6209	. . . . . . . . . . . . . . . . . . . 20 |- ( ( F Isom _E , R ( dom F , A ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c _E d <-> ( F ` c ) R ( F ` d ) ) )
184	182, 183	sylancom 667	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c _E d <-> ( F ` c ) R ( F ` d ) ) )
185	181, 184	syl5bbr 259	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c e. d <-> ( F ` c ) R ( F ` d ) ) )
186	152	adantrr 716	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( x o. F ) : dom F --> B )
187		simprr 756	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> d e. dom F )
188		fvco3 5943	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( x o. F ) : dom F --> B /\ d e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` d ) = ( `' G ` ( ( x o. F ) ` d ) ) )
189	186, 187, 188	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( `' G o. ( x o. F ) ) ` d ) = ( `' G ` ( ( x o. F ) ` d ) ) )
190	162	adantrr 716	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( y o. F ) : dom F --> B )
191		fvco3 5943	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y o. F ) : dom F --> B /\ d e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` d ) = ( `' G ` ( ( y o. F ) ` d ) ) )
192	190, 187, 191	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( `' G o. ( y o. F ) ) ` d ) = ( `' G ` ( ( y o. F ) ` d ) ) )
193	189, 192	eqeq12d 2489	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) <-> ( `' G ` ( ( x o. F ) ` d ) ) = ( `' G ` ( ( y o. F ) ` d ) ) ) )
194	30	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> G : dom G -1-1-onto-> B )
195		f1of1 5814	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' G : B -1-1-onto-> dom G -> `' G : B -1-1-> dom G )
196	194, 19, 195	3syl 20	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> `' G : B -1-1-> dom G )
197	186, 187	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( x o. F ) ` d ) e. B )
198	190, 187	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( y o. F ) ` d ) e. B )
199		f1fveq 6157	. . . . . . . . . . . . . . . . . . . 20 |- ( ( `' G : B -1-1-> dom G /\ ( ( ( x o. F ) ` d ) e. B /\ ( ( y o. F ) ` d ) e. B ) ) -> ( ( `' G ` ( ( x o. F ) ` d ) ) = ( `' G ` ( ( y o. F ) ` d ) ) <-> ( ( x o. F ) ` d ) = ( ( y o. F ) ` d ) ) )
200	196, 197, 198, 199	syl12anc 1226	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( `' G ` ( ( x o. F ) ` d ) ) = ( `' G ` ( ( y o. F ) ` d ) ) <-> ( ( x o. F ) ` d ) = ( ( y o. F ) ` d ) ) )
201		fvco3 5943	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
202	136, 187, 201	sylancr 663	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
203		fvco3 5943	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
204	136, 187, 203	sylancr 663	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
205	202, 204	eqeq12d 2489	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( ( x o. F ) ` d ) = ( ( y o. F ) ` d ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
206	193, 200, 205	3bitrd 279	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
207	185, 206	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
208	207	anassrs 648	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) /\ d e. dom F ) -> ( ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
209	208	ralbidva 2900	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
210	180, 209	bitr4d 256	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) )
211	170, 210	anbi12d 710	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
212	211	rexbidva 2970	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
213	115, 127, 212	3bitr4rd 286	. . . . . . . . . . 11 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) ) )
214	84, 88, 213	3bitr3d 283	. . . . . . . . . 10 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) ) )
215	214	ex 434	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( x e. U /\ y e. U ) -> ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) ) ) )
216	215	pm5.32rd 640	. . . . . . . 8 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) <-> ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) ) )
217	216	opabbidv 4510	. . . . . . 7 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { <. x , y >. | ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) } = { <. x , y >. | ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) } )
218		wemapwe.t	. . . . . . . . 9 |- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) }
219		df-xp 5005	. . . . . . . . 9 |- ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
220	218, 219	ineq12i 3698	. . . . . . . 8 |- ( T i^i ( U X. U ) ) = ( { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } )
221		inopab 5132	. . . . . . . 8 |- ( { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } ) = { <. x , y >. | ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) }
222	220, 221	eqtri 2496	. . . . . . 7 |- ( T i^i ( U X. U ) ) = { <. x , y >. | ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) }
223	219	ineq2i 3697	. . . . . . . 8 |- ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) = ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } )
224		inopab 5132	. . . . . . . 8 |- ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } ) = { <. x , y >. | ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) }
225	223, 224	eqtri 2496	. . . . . . 7 |- ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) = { <. x , y >. | ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) }
226	217, 222, 225	3eqtr4g 2533	. . . . . 6 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) = ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) )
227		weeq1 4867	. . . . . 6 |- ( ( T i^i ( U X. U ) ) = ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) -> ( ( T i^i ( U X. U ) ) We U <-> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U ) )
228	226, 227	syl 16	. . . . 5 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( T i^i ( U X. U ) ) We U <-> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U ) )
229	73, 228	mpbird 232	. . . 4 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) We U )
230		weinxp 5066	. . . 4 |- ( T We U <-> ( T i^i ( U X. U ) ) We U )
231	229, 230	sylibr 212	. . 3 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> T We U )
232	231	ex 434	. 2 |- ( ph -> ( ( B e. _V /\ A e. _V ) -> T We U ) )
233		we0 4874	. . 3 |- T We (/)
234		elmapex 7439	. . . . . . . . 9 |- ( x e. ( B ^m A ) -> ( B e. _V /\ A e. _V ) )
235	234	con3i 135	. . . . . . . 8 |- ( -. ( B e. _V /\ A e. _V ) -> -. x e. ( B ^m A ) )
236	235	pm2.21d 106	. . . . . . 7 |- ( -. ( B e. _V /\ A e. _V ) -> ( x e. ( B ^m A ) -> -. x finSupp Z ) )
237	236	ralrimiv 2876	. . . . . 6 |- ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
238		rabeq0 3807	. . . . . 6 |- ( { x e. ( B ^m A ) | x finSupp Z } = (/) <-> A. x e. ( B ^m A ) -. x finSupp Z )
239	237, 238	sylibr 212	. . . . 5 |- ( -. ( B e. _V /\ A e. _V ) -> { x e. ( B ^m A ) | x finSupp Z } = (/) )
240	1, 239	syl5eq 2520	. . . 4 |- ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
241		weeq2 4868	. . . 4 |- ( U = (/) -> ( T We U <-> T We (/) ) )
242	240, 241	syl 16	. . 3 |- ( -. ( B e. _V /\ A e. _V ) -> ( T We U <-> T We (/) ) )
243	233, 242	mpbiri 233	. 2 |- ( -. ( B e. _V /\ A e. _V ) -> T We U )
244	232, 243	pm2.61d1 159	1 |- ( ph -> T We U )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113   i^i cin 3475   (/)c0 3785   class class class wbr 4447   {copab 4504   |-> cmpt 4505   _E cep 4789   We wwe 4837   Ord word 4877   Oncon0 4878   X. cxp 4997   `'ccnv 4998   dom cdm 4999   ran crn 5000   o. ccom 5003   Fn wfn 5582   -->wf 5583   -1-1->wf1 5584   -onto->wfo 5585   -1-1-onto->wf1o 5586   ` cfv 5587   Isom wiso 5588  (class class class)co 6283   ^o coe 7129   ^m cmap 7420   finSupp cfsupp 7828  OrdIsocoi 7933   CNF ccnf 8077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-isom 5596  df-riota 6244  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-om 6680  df-1st 6784  df-2nd 6785  df-supp 6902  df-recs 7042  df-rdg 7076  df-seqom 7113  df-1o 7130  df-2o 7131  df-oadd 7134  df-omul 7135  df-oexp 7136  df-er 7311  df-map 7422  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fsupp 7829  df-oi 7934  df-cnf 8078

This theorem is referenced by:  ltbwe  17924