Theorem wemapwe 8210

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 2422	. . . . . . . . 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 2422	. . . . . . . . 9 |- ( `' G ` Z ) = ( `' G ` Z )
4		simprr 764	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> A e. _V )
5		wemapwe.2	. . . . . . . . . . . 12 |- ( ph -> R We A )
6	5	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> R We A )
7		wemapwe.5	. . . . . . . . . . . 12 |- F = OrdIso ( R , A )
8	7	oiiso 8061	. . . . . . . . . . 11 |- ( ( A e. _V /\ R We A ) -> F Isom _E , R ( dom F , A ) )
9	4, 6, 8	syl2anc 665	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F Isom _E , R ( dom F , A ) )
10		isof1o 6231	. . . . . . . . . 10 |- ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A )
11	9, 10	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F : dom F -1-1-onto-> A )
12		simprl 762	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B e. _V )
13		wemapwe.3	. . . . . . . . . . . 12 |- ( ph -> S We B )
14	13	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> S We B )
15		wemapwe.6	. . . . . . . . . . . 12 |- G = OrdIso ( S , B )
16	15	oiiso 8061	. . . . . . . . . . 11 |- ( ( B e. _V /\ S We B ) -> G Isom _E , S ( dom G , B ) )
17	12, 14, 16	syl2anc 665	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G Isom _E , S ( dom G , B ) )
18		isof1o 6231	. . . . . . . . . 10 |- ( G Isom _E , S ( dom G , B ) -> G : dom G -1-1-onto-> B )
19		f1ocnv 5843	. . . . . . . . . 10 |- ( G : dom G -1-1-onto-> B -> `' G : B -1-1-onto-> dom G )
20	17, 18, 19	3syl 18	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> `' G : B -1-1-onto-> dom G )
21	7	oiexg 8059	. . . . . . . . . . 11 |- ( A e. _V -> F e. _V )
22	21	ad2antll 733	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F e. _V )
23		dmexg 6738	. . . . . . . . . 10 |- ( F e. _V -> dom F e. _V )
24	22, 23	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. _V )
25	15	oiexg 8059	. . . . . . . . . . 11 |- ( B e. _V -> G e. _V )
26	25	ad2antrl 732	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G e. _V )
27		dmexg 6738	. . . . . . . . . 10 |- ( G e. _V -> dom G e. _V )
28	26, 27	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. _V )
29		wemapwe.7	. . . . . . . . . 10 |- Z = ( G ` (/) )
30	17, 18	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G : dom G -1-1-onto-> B )
31		f1ofo 5838	. . . . . . . . . . . . . . 15 |- ( G : dom G -1-1-onto-> B -> G : dom G -onto-> B )
32		forn 5813	. . . . . . . . . . . . . . 15 |- ( G : dom G -onto-> B -> ran G = B )
33	30, 31, 32	3syl 18	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G = B )
34		wemapwe.4	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= (/) )
35	34	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B =/= (/) )
36	33, 35	eqnetrd 2713	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G =/= (/) )
37		dm0rn0 5070	. . . . . . . . . . . . . 14 |- ( dom G = (/) <-> ran G = (/) )
38	37	necon3bii 2688	. . . . . . . . . . . . 13 |- ( dom G =/= (/) <-> ran G =/= (/) )
39	36, 38	sylibr 215	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G =/= (/) )
40	15	oicl 8053	. . . . . . . . . . . . 13 |- Ord dom G
41		ord0eln0 5496	. . . . . . . . . . . . 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 215	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> (/) e. dom G )
44	15	oif 8054	. . . . . . . . . . . 12 |- G : dom G --> B
45	44	ffvelrni 6036	. . . . . . . . . . 11 |- ( (/) e. dom G -> ( G ` (/) ) e. B )
46	43, 45	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( G ` (/) ) e. B )
47	29, 46	syl5eqel 2511	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> Z e. B )
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 7930	. . . . . . . 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 2422	. . . . . . . . . . 11 |- { x e. ( dom G ^m dom F ) | x finSupp (/) } = { x e. ( dom G ^m dom F ) | x finSupp (/) }
50	15	oion 8060	. . . . . . . . . . . 12 |- ( B e. _V -> dom G e. On )
51	50	ad2antrl 732	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. On )
52	7	oion 8060	. . . . . . . . . . . 12 |- ( A e. _V -> dom F e. On )
53	52	ad2antll 733	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. On )
54	49, 51, 53	cantnfdm 8177	. . . . . . . . . 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 5884	. . . . . . . . . . . . 13 |- ( `' G ` Z ) = ( `' G ` ( G ` (/) ) )
56		f1ocnvfv1 6190	. . . . . . . . . . . . . 14 |- ( ( G : dom G -1-1-onto-> B /\ (/) e. dom G ) -> ( `' G ` ( G ` (/) ) ) = (/) )
57	30, 43, 56	syl2anc 665	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` ( G ` (/) ) ) = (/) )
58	55, 57	syl5eq 2475	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` Z ) = (/) )
59	58	breq2d 4435	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( x finSupp ( `' G ` Z ) <-> x finSupp (/) ) )
60	59	rabbidv 3071	. . . . . . . . . 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 2466	. . . . . . . . 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 5824	. . . . . . . . 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 17	. . . . . . . 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 235	. . . . . . 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 2422	. . . . . . . . 9 |- dom ( dom G CNF dom F ) = dom ( dom G CNF dom F )
66		eqid 2422	. . . . . . . . 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 8207	. . . . . . . 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 460	. . . . . . 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 2422	. . . . . . . 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 6259	. . . . . . 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 62	. . . . . 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 4921	. . . . . 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 199	. . . . 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 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F : dom F -1-1-onto-> A )
75		f1ofn 5832	. . . . . . . . . . . 12 |- ( F : dom F -1-1-onto-> A -> F Fn dom F )
76		fveq2 5881	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
77		fveq2 5881	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
78	76, 77	breq12d 4436	. . . . . . . . . . . . . 14 |- ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
79		breq1 4426	. . . . . . . . . . . . . . . 16 |- ( z = ( F ` c ) -> ( z R w <-> ( F ` c ) R w ) )
80	79	imbi1d 318	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( ( z R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
81	80	ralbidv 2861	. . . . . . . . . . . . . 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 715	. . . . . . . . . . . . 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 6039	. . . . . . . . . . . 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 18	. . . . . . . . . . 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 5838	. . . . . . . . . . . . 13 |- ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
86		forn 5813	. . . . . . . . . . . . 13 |- ( F : dom F -onto-> A -> ran F = A )
87	74, 85, 86	3syl 18	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ran F = A )
88	87	rexeqdv 3029	. . . . . . . . . . 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 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> G e. _V )
90		cnvexg 6753	. . . . . . . . . . . . . . 15 |- ( G e. _V -> `' G e. _V )
91	89, 90	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> `' G e. _V )
92		vex 3083	. . . . . . . . . . . . . . 15 |- x e. _V
93	22	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F e. _V )
94		coexg 6758	. . . . . . . . . . . . . . 15 |- ( ( x e. _V /\ F e. _V ) -> ( x o. F ) e. _V )
95	92, 93, 94	sylancr 667	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( x o. F ) e. _V )
96		coexg 6758	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( x o. F ) e. _V ) -> ( `' G o. ( x o. F ) ) e. _V )
97	91, 95, 96	syl2anc 665	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( x o. F ) ) e. _V )
98		vex 3083	. . . . . . . . . . . . . . 15 |- y e. _V
99		coexg 6758	. . . . . . . . . . . . . . 15 |- ( ( y e. _V /\ F e. _V ) -> ( y o. F ) e. _V )
100	98, 93, 99	sylancr 667	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( y o. F ) e. _V )
101		coexg 6758	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( y o. F ) e. _V ) -> ( `' G o. ( y o. F ) ) e. _V )
102	91, 100, 101	syl2anc 665	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( y o. F ) ) e. _V )
103		fveq1 5880	. . . . . . . . . . . . . . . . 17 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
104		fveq1 5880	. . . . . . . . . . . . . . . . 17 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
105		eleq12 2497	. . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . 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 5880	. . . . . . . . . . . . . . . . . . 19 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
108		fveq1 5880	. . . . . . . . . . . . . . . . . . 19 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
109	107, 108	eqeqan12d 2445	. . . . . . . . . . . . . . . . . 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 317	. . . . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . 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 2936	. . . . . . . . . . . . . 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 4734	. . . . . . . . . . . . 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 665	. . . . . . . . . . . 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 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. U )
117		coeq1 5011	. . . . . . . . . . . . . . . 16 |- ( f = x -> ( f o. F ) = ( x o. F ) )
118	117	coeq2d 5016	. . . . . . . . . . . . . . 15 |- ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
119		eqid 2422	. . . . . . . . . . . . . . 15 |- ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
120	118, 119	fvmptg 5962	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 764	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
123		coeq1 5011	. . . . . . . . . . . . . . . 16 |- ( f = y -> ( f o. F ) = ( y o. F ) )
124	123	coeq2d 5016	. . . . . . . . . . . . . . 15 |- ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
125	124, 119	fvmptg 5962	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 4436	. . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . 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 6236	. . . . . . . . . . . . . . . . . 18 |- ( G Isom _E , S ( dom G , B ) -> `' G Isom S , _E ( B , dom G ) )
130	128, 129	syl 17	. . . . . . . . . . . . . . . . 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 3546	. . . . . . . . . . . . . . . . . . . . 21 |- { x e. ( B ^m A ) | x finSupp Z } C_ ( B ^m A )
132	1, 131	eqsstri 3494	. . . . . . . . . . . . . . . . . . . 20 |- U C_ ( B ^m A )
133	132, 116	sseldi 3462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
134		elmapi 7504	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( B ^m A ) -> x : A --> B )
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x : A --> B )
136	7	oif 8054	. . . . . . . . . . . . . . . . . . 19 |- F : dom F --> A
137	136	ffvelrni 6036	. . . . . . . . . . . . . . . . . 18 |- ( c e. dom F -> ( F ` c ) e. A )
138		ffvelrn 6035	. . . . . . . . . . . . . . . . . 18 |- ( ( x : A --> B /\ ( F ` c ) e. A ) -> ( x ` ( F ` c ) ) e. B )
139	135, 137, 138	syl2an 479	. . . . . . . . . . . . . . . . 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 3462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
141		elmapi 7504	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( B ^m A ) -> y : A --> B )
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y : A --> B )
143		ffvelrn 6035	. . . . . . . . . . . . . . . . . 18 |- ( ( y : A --> B /\ ( F ` c ) e. A ) -> ( y ` ( F ` c ) ) e. B )
144	142, 137, 143	syl2an 479	. . . . . . . . . . . . . . . . 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 6232	. . . . . . . . . . . . . . . . 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 1262	. . . . . . . . . . . . . . . 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 5891	. . . . . . . . . . . . . . . . 17 |- ( `' G ` ( y ` ( F ` c ) ) ) e. _V
148	147	epelc 4766	. . . . . . . . . . . . . . . 16 |- ( ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) )
149	146, 148	syl6bb 264	. . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> x : A --> B )
151		fco 5756	. . . . . . . . . . . . . . . . . . 19 |- ( ( x : A --> B /\ F : dom F --> A ) -> ( x o. F ) : dom F --> B )
152	150, 136, 151	sylancl 666	. . . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> c e. dom F )
156		fvco3 5958	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
157	136, 155, 156	sylancr 667	. . . . . . . . . . . . . . . . . 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 5885	. . . . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> y : A --> B )
161		fco 5756	. . . . . . . . . . . . . . . . . . 19 |- ( ( y : A --> B /\ F : dom F --> A ) -> ( y o. F ) : dom F --> B )
162	160, 136, 161	sylancl 666	. . . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
166	136, 155, 165	sylancr 667	. . . . . . . . . . . . . . . . . 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 5885	. . . . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . 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 259	. . . . . . . . . . . . . 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 3028	. . . . . . . . . . . . . . . . 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 4427	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
173		fveq2 5881	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
174		fveq2 5881	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
175	173, 174	eqeq12d 2444	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( x ` w ) = ( y ` w ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
176	172, 175	imbi12d 321	. . . . . . . . . . . . . . . . . . 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 6040	. . . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . . . 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 258	. . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . 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 4767	. . . . . . . . . . . . . . . . . . 19 |- ( c _E d <-> c e. d )
182	9	ad2antrr 730	. . . . . . . . . . . . . . . . . . . 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 6232	. . . . . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . . . . 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 262	. . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . . 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 764	. . . . . . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . 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 2444	. . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . . 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 5830	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' G : B -1-1-onto-> dom G -> `' G : B -1-1-> dom G )
196	194, 19, 195	3syl 18	. . . . . . . . . . . . . . . . . . . 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 6038	. . . . . . . . . . . . . . . . . . . 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 6038	. . . . . . . . . . . . . . . . . . . 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 6178	. . . . . . . . . . . . . . . . . . . 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 1262	. . . . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
202	136, 187, 201	sylancr 667	. . . . . . . . . . . . . . . . . . . 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 5958	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
204	136, 187, 203	sylancr 667	. . . . . . . . . . . . . . . . . . . 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 2444	. . . . . . . . . . . . . . . . . . 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 282	. . . . . . . . . . . . . . . . . 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 321	. . . . . . . . . . . . . . . . 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 652	. . . . . . . . . . . . . . . 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 2858	. . . . . . . . . . . . . . 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 259	. . . . . . . . . . . . . 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 715	. . . . . . . . . . . . 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 2933	. . . . . . . . . . . 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 289	. . . . . . . . . . 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 286	. . . . . . . . . 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 435	. . . . . . . . 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 644	. . . . . . . 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 4487	. . . . . . 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 4859	. . . . . . . . 9 |- ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
220	218, 219	ineq12i 3662	. . . . . . . 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 4984	. . . . . . . 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 2451	. . . . . . 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 3661	. . . . . . . 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 4984	. . . . . . . 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 2451	. . . . . . 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 2488	. . . . . 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 4841	. . . . . 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 17	. . . . 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 235	. . . 4 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) We U )
230		weinxp 4921	. . . 4 |- ( T We U <-> ( T i^i ( U X. U ) ) We U )
231	229, 230	sylibr 215	. . 3 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> T We U )
232	231	ex 435	. 2 |- ( ph -> ( ( B e. _V /\ A e. _V ) -> T We U ) )
233		we0 4848	. . 3 |- T We (/)
234		elmapex 7503	. . . . . . . . 9 |- ( x e. ( B ^m A ) -> ( B e. _V /\ A e. _V ) )
235	234	con3i 140	. . . . . . . 8 |- ( -. ( B e. _V /\ A e. _V ) -> -. x e. ( B ^m A ) )
236	235	pm2.21d 109	. . . . . . 7 |- ( -. ( B e. _V /\ A e. _V ) -> ( x e. ( B ^m A ) -> -. x finSupp Z ) )
237	236	ralrimiv 2834	. . . . . 6 |- ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
238		rabeq0 3784	. . . . . 6 |- ( { x e. ( B ^m A ) | x finSupp Z } = (/) <-> A. x e. ( B ^m A ) -. x finSupp Z )
239	237, 238	sylibr 215	. . . . 5 |- ( -. ( B e. _V /\ A e. _V ) -> { x e. ( B ^m A ) | x finSupp Z } = (/) )
240	1, 239	syl5eq 2475	. . . 4 |- ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
241		weeq2 4842	. . . 4 |- ( U = (/) -> ( T We U <-> T We (/) ) )
242	240, 241	syl 17	. . 3 |- ( -. ( B e. _V /\ A e. _V ) -> ( T We U <-> T We (/) ) )
243	233, 242	mpbiri 236	. 2 |- ( -. ( B e. _V /\ A e. _V ) -> T We U )
244	232, 243	pm2.61d1 162	1 |- ( ph -> T We U )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   =/= wne 2614   A.wral 2771   E.wrex 2772   {crab 2775   _Vcvv 3080   i^i cin 3435   (/)c0 3761   class class class wbr 4423   {copab 4481   |-> cmpt 4482   _E cep 4762   We wwe 4811   X. cxp 4851   `'ccnv 4852   dom cdm 4853   ran crn 4854   o. ccom 4857   Ord word 5441   Oncon0 5442   Fn wfn 5596   -->wf 5597   -1-1->wf1 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600   ` cfv 5601   Isom wiso 5602  (class class class)co 6305   ^o coe 7192   ^m cmap 7483   finSupp cfsupp 7892  OrdIsocoi 8033   CNF ccnf 8174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-seqom 7176  df-1o 7193  df-2o 7194  df-oadd 7197  df-omul 7198  df-oexp 7199  df-er 7374  df-map 7485  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-fsupp 7893  df-oi 8034  df-cnf 8175

This theorem is referenced by:  ltbwe  18695