Theorem wemapwe 8156

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 2457	. . . . . . . . 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 2457	. . . . . . . . 9 |- ( `' G ` Z ) = ( `' G ` Z )
4		simprr 757	. . . . . . . . . . 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 7980	. . . . . . . . . . 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 6222	. . . . . . . . . 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 756	. . . . . . . . . . 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 7980	. . . . . . . . . . 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 6222	. . . . . . . . . 10 |- ( G Isom _E , S ( dom G , B ) -> G : dom G -1-1-onto-> B )
19		f1ocnv 5834	. . . . . . . . . 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 7978	. . . . . . . . . . 11 |- ( A e. _V -> F e. _V )
22	21	ad2antll 728	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F e. _V )
23		dmexg 6730	. . . . . . . . . 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 7978	. . . . . . . . . . 11 |- ( B e. _V -> G e. _V )
26	25	ad2antrl 727	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G e. _V )
27		dmexg 6730	. . . . . . . . . 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 5829	. . . . . . . . . . . . . . 15 |- ( G : dom G -1-1-onto-> B -> G : dom G -onto-> B )
32		forn 5804	. . . . . . . . . . . . . . 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 2750	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G =/= (/) )
37		dm0rn0 5229	. . . . . . . . . . . . . 14 |- ( dom G = (/) <-> ran G = (/) )
38	37	necon3bii 2725	. . . . . . . . . . . . 13 |- ( dom G =/= (/) <-> ran G =/= (/) )
39	36, 38	sylibr 212	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G =/= (/) )
40	15	oicl 7972	. . . . . . . . . . . . 13 |- Ord dom G
41		ord0eln0 4941	. . . . . . . . . . . . 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 7973	. . . . . . . . . . . 12 |- G : dom G --> B
45	44	ffvelrni 6031	. . . . . . . . . . 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 2549	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> Z e. B )
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 7885	. . . . . . . 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 2457	. . . . . . . . . . 11 |- { x e. ( dom G ^m dom F ) | x finSupp (/) } = { x e. ( dom G ^m dom F ) | x finSupp (/) }
50	15	oion 7979	. . . . . . . . . . . 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 7979	. . . . . . . . . . . 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 8098	. . . . . . . . . 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 5875	. . . . . . . . . . . . 13 |- ( `' G ` Z ) = ( `' G ` ( G ` (/) ) )
56		f1ocnvfv1 6183	. . . . . . . . . . . . . 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 2510	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` Z ) = (/) )
59	58	breq2d 4468	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( x finSupp ( `' G ` Z ) <-> x finSupp (/) ) )
60	59	rabbidv 3101	. . . . . . . . . 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 2501	. . . . . . . . 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 5815	. . . . . . . . 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 2457	. . . . . . . . 9 |- dom ( dom G CNF dom F ) = dom ( dom G CNF dom F )
66		eqid 2457	. . . . . . . . 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 8130	. . . . . . . 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 2457	. . . . . . . 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 6250	. . . . . . 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 5076	. . . . . 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 5823	. . . . . . . . . . . 12 |- ( F : dom F -1-1-onto-> A -> F Fn dom F )
76		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
77		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
78	76, 77	breq12d 4469	. . . . . . . . . . . . . 14 |- ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
79		breq1 4459	. . . . . . . . . . . . . . . 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 2896	. . . . . . . . . . . . . 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 6034	. . . . . . . . . . . 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 5829	. . . . . . . . . . . . 13 |- ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
86		forn 5804	. . . . . . . . . . . . 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 3061	. . . . . . . . . . 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 6745	. . . . . . . . . . . . . . 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 3112	. . . . . . . . . . . . . . 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 6750	. . . . . . . . . . . . . . 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 6750	. . . . . . . . . . . . . 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 3112	. . . . . . . . . . . . . . 15 |- y e. _V
99		coexg 6750	. . . . . . . . . . . . . . 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 6750	. . . . . . . . . . . . . 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 5871	. . . . . . . . . . . . . . . . 17 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
104		fveq1 5871	. . . . . . . . . . . . . . . . 17 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
105		eleq12 2533	. . . . . . . . . . . . . . . . 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 5871	. . . . . . . . . . . . . . . . . . 19 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
108		fveq1 5871	. . . . . . . . . . . . . . . . . . 19 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
109	107, 108	eqeqan12d 2480	. . . . . . . . . . . . . . . . . 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 2896	. . . . . . . . . . . . . . . 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 2968	. . . . . . . . . . . . . 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 4770	. . . . . . . . . . . . 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 756	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. U )
117		coeq1 5170	. . . . . . . . . . . . . . . 16 |- ( f = x -> ( f o. F ) = ( x o. F ) )
118	117	coeq2d 5175	. . . . . . . . . . . . . . 15 |- ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
119		eqid 2457	. . . . . . . . . . . . . . 15 |- ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
120	118, 119	fvmptg 5954	. . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
123		coeq1 5170	. . . . . . . . . . . . . . . 16 |- ( f = y -> ( f o. F ) = ( y o. F ) )
124	123	coeq2d 5175	. . . . . . . . . . . . . . 15 |- ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
125	124, 119	fvmptg 5954	. . . . . . . . . . . . . 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 4469	. . . . . . . . . . . 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 6227	. . . . . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . . . . . . . . . . 21 |- { x e. ( B ^m A ) | x finSupp Z } C_ ( B ^m A )
132	1, 131	eqsstri 3529	. . . . . . . . . . . . . . . . . . . 20 |- U C_ ( B ^m A )
133	132, 116	sseldi 3497	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
134		elmapi 7459	. . . . . . . . . . . . . . . . . . 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 7973	. . . . . . . . . . . . . . . . . . 19 |- F : dom F --> A
137	136	ffvelrni 6031	. . . . . . . . . . . . . . . . . 18 |- ( c e. dom F -> ( F ` c ) e. A )
138		ffvelrn 6030	. . . . . . . . . . . . . . . . . 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 3497	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
141		elmapi 7459	. . . . . . . . . . . . . . . . . . 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 6030	. . . . . . . . . . . . . . . . . 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 6223	. . . . . . . . . . . . . . . . 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 5882	. . . . . . . . . . . . . . . . 17 |- ( `' G ` ( y ` ( F ` c ) ) ) e. _V
148	147	epelc 4802	. . . . . . . . . . . . . . . 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 5747	. . . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . . . . 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 5747	. . . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . . . . 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 2539	. . . . . . . . . . . . . . 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 3060	. . . . . . . . . . . . . . . . 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 4460	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
173		fveq2 5872	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
174		fveq2 5872	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
175	173, 174	eqeq12d 2479	. . . . . . . . . . . . . . . . . . . 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 6035	. . . . . . . . . . . . . . . . . 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 4803	. . . . . . . . . . . . . . . . . . 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 6223	. . . . . . . . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . . . . 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 2479	. . . . . . . . . . . . . . . . . . 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 5821	. . . . . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . . . . . 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 6171	. . . . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . . . . . . . . . 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 2479	. . . . . . . . . . . . . . . . . . 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 2893	. . . . . . . . . . . . . . 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 2965	. . . . . . . . . . . 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 4520	. . . . . . 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 5014	. . . . . . . . 9 |- ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
220	218, 219	ineq12i 3694	. . . . . . . 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 5143	. . . . . . . 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 2486	. . . . . . 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 3693	. . . . . . . 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 5143	. . . . . . . 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 2486	. . . . . . 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 2523	. . . . . 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 4876	. . . . . 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 5076	. . . 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 4883	. . 3 |- T We (/)
234		elmapex 7458	. . . . . . . . 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 2869	. . . . . 6 |- ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
238		rabeq0 3816	. . . . . 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 2510	. . . 4 |- ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
241		weeq2 4877	. . . 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 1395   e. wcel 1819   =/= wne 2652   A.wral 2807   E.wrex 2808   {crab 2811   _Vcvv 3109   i^i cin 3470   (/)c0 3793   class class class wbr 4456   {copab 4514   |-> cmpt 4515   _E cep 4798   We wwe 4846   Ord word 4886   Oncon0 4887   X. cxp 5006   `'ccnv 5007   dom cdm 5008   ran crn 5009   o. ccom 5012   Fn wfn 5589   -->wf 5590   -1-1->wf1 5591   -onto->wfo 5592   -1-1-onto->wf1o 5593   ` cfv 5594   Isom wiso 5595  (class class class)co 6296   ^o coe 7147   ^m cmap 7438   finSupp cfsupp 7847  OrdIsocoi 7952   CNF ccnf 8095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-seqom 7131  df-1o 7148  df-2o 7149  df-oadd 7152  df-omul 7153  df-oexp 7154  df-er 7329  df-map 7440  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-oi 7953  df-cnf 8096

This theorem is referenced by:  ltbwe  18264