Theorem wemapwe 8170

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 2402	. . . . . . . . 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 2402	. . . . . . . . 9 |- ( `' G ` Z ) = ( `' G ` Z )
4		simprr 758	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> A e. _V )
5		wemapwe.2	. . . . . . . . . . . 12 |- ( ph -> R We A )
6	5	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> R We A )
7		wemapwe.5	. . . . . . . . . . . 12 |- F = OrdIso ( R , A )
8	7	oiiso 7995	. . . . . . . . . . 11 |- ( ( A e. _V /\ R We A ) -> F Isom _E , R ( dom F , A ) )
9	4, 6, 8	syl2anc 659	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F Isom _E , R ( dom F , A ) )
10		isof1o 6203	. . . . . . . . . 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 756	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B e. _V )
13		wemapwe.3	. . . . . . . . . . . 12 |- ( ph -> S We B )
14	13	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> S We B )
15		wemapwe.6	. . . . . . . . . . . 12 |- G = OrdIso ( S , B )
16	15	oiiso 7995	. . . . . . . . . . 11 |- ( ( B e. _V /\ S We B ) -> G Isom _E , S ( dom G , B ) )
17	12, 14, 16	syl2anc 659	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G Isom _E , S ( dom G , B ) )
18		isof1o 6203	. . . . . . . . . 10 |- ( G Isom _E , S ( dom G , B ) -> G : dom G -1-1-onto-> B )
19		f1ocnv 5810	. . . . . . . . . 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 7993	. . . . . . . . . . 11 |- ( A e. _V -> F e. _V )
22	21	ad2antll 727	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F e. _V )
23		dmexg 6714	. . . . . . . . . 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 7993	. . . . . . . . . . 11 |- ( B e. _V -> G e. _V )
26	25	ad2antrl 726	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G e. _V )
27		dmexg 6714	. . . . . . . . . 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 5805	. . . . . . . . . . . . . . 15 |- ( G : dom G -1-1-onto-> B -> G : dom G -onto-> B )
32		forn 5780	. . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B =/= (/) )
36	33, 35	eqnetrd 2696	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G =/= (/) )
37		dm0rn0 5039	. . . . . . . . . . . . . 14 |- ( dom G = (/) <-> ran G = (/) )
38	37	necon3bii 2671	. . . . . . . . . . . . 13 |- ( dom G =/= (/) <-> ran G =/= (/) )
39	36, 38	sylibr 212	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G =/= (/) )
40	15	oicl 7987	. . . . . . . . . . . . 13 |- Ord dom G
41		ord0eln0 5463	. . . . . . . . . . . . 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 7988	. . . . . . . . . . . 12 |- G : dom G --> B
45	44	ffvelrni 6007	. . . . . . . . . . 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 2494	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> Z e. B )
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 7900	. . . . . . . 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 2402	. . . . . . . . . . 11 |- { x e. ( dom G ^m dom F ) | x finSupp (/) } = { x e. ( dom G ^m dom F ) | x finSupp (/) }
50	15	oion 7994	. . . . . . . . . . . 12 |- ( B e. _V -> dom G e. On )
51	50	ad2antrl 726	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. On )
52	7	oion 7994	. . . . . . . . . . . 12 |- ( A e. _V -> dom F e. On )
53	52	ad2antll 727	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. On )
54	49, 51, 53	cantnfdm 8112	. . . . . . . . . 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 5851	. . . . . . . . . . . . 13 |- ( `' G ` Z ) = ( `' G ` ( G ` (/) ) )
56		f1ocnvfv1 6162	. . . . . . . . . . . . . 14 |- ( ( G : dom G -1-1-onto-> B /\ (/) e. dom G ) -> ( `' G ` ( G ` (/) ) ) = (/) )
57	30, 43, 56	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` ( G ` (/) ) ) = (/) )
58	55, 57	syl5eq 2455	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` Z ) = (/) )
59	58	breq2d 4406	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( x finSupp ( `' G ` Z ) <-> x finSupp (/) ) )
60	59	rabbidv 3050	. . . . . . . . . 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 2446	. . . . . . . . 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 5791	. . . . . . . . 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 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 2402	. . . . . . . . 9 |- dom ( dom G CNF dom F ) = dom ( dom G CNF dom F )
66		eqid 2402	. . . . . . . . 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 8144	. . . . . . . 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 457	. . . . . . 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 2402	. . . . . . . 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 6231	. . . . . . 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 59	. . . . . 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 4890	. . . . . 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 463	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F : dom F -1-1-onto-> A )
75		f1ofn 5799	. . . . . . . . . . . 12 |- ( F : dom F -1-1-onto-> A -> F Fn dom F )
76		fveq2 5848	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
77		fveq2 5848	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
78	76, 77	breq12d 4407	. . . . . . . . . . . . . 14 |- ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
79		breq1 4397	. . . . . . . . . . . . . . . 16 |- ( z = ( F ` c ) -> ( z R w <-> ( F ` c ) R w ) )
80	79	imbi1d 315	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( ( z R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
81	80	ralbidv 2842	. . . . . . . . . . . . . 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 709	. . . . . . . . . . . . 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 6010	. . . . . . . . . . . 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 5805	. . . . . . . . . . . . 13 |- ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
86		forn 5780	. . . . . . . . . . . . 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 3010	. . . . . . . . . . 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 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> G e. _V )
90		cnvexg 6729	. . . . . . . . . . . . . . 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 3061	. . . . . . . . . . . . . . 15 |- x e. _V
93	22	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F e. _V )
94		coexg 6734	. . . . . . . . . . . . . . 15 |- ( ( x e. _V /\ F e. _V ) -> ( x o. F ) e. _V )
95	92, 93, 94	sylancr 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( x o. F ) e. _V )
96		coexg 6734	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( x o. F ) e. _V ) -> ( `' G o. ( x o. F ) ) e. _V )
97	91, 95, 96	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( x o. F ) ) e. _V )
98		vex 3061	. . . . . . . . . . . . . . 15 |- y e. _V
99		coexg 6734	. . . . . . . . . . . . . . 15 |- ( ( y e. _V /\ F e. _V ) -> ( y o. F ) e. _V )
100	98, 93, 99	sylancr 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( y o. F ) e. _V )
101		coexg 6734	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( y o. F ) e. _V ) -> ( `' G o. ( y o. F ) ) e. _V )
102	91, 100, 101	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( y o. F ) ) e. _V )
103		fveq1 5847	. . . . . . . . . . . . . . . . 17 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
104		fveq1 5847	. . . . . . . . . . . . . . . . 17 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
105		eleq12 2478	. . . . . . . . . . . . . . . . 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 475	. . . . . . . . . . . . . . . 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 5847	. . . . . . . . . . . . . . . . . . 19 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
108		fveq1 5847	. . . . . . . . . . . . . . . . . . 19 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
109	107, 108	eqeqan12d 2425	. . . . . . . . . . . . . . . . . 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 314	. . . . . . . . . . . . . . . . 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 2842	. . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . 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 2917	. . . . . . . . . . . . . 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 4703	. . . . . . . . . . . . 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 659	. . . . . . . . . . . 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 4980	. . . . . . . . . . . . . . . 16 |- ( f = x -> ( f o. F ) = ( x o. F ) )
118	117	coeq2d 4985	. . . . . . . . . . . . . . 15 |- ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
119		eqid 2402	. . . . . . . . . . . . . . 15 |- ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
120	118, 119	fvmptg 5929	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 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 758	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
123		coeq1 4980	. . . . . . . . . . . . . . . 16 |- ( f = y -> ( f o. F ) = ( y o. F ) )
124	123	coeq2d 4985	. . . . . . . . . . . . . . 15 |- ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
125	124, 119	fvmptg 5929	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 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 4407	. . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . 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 6208	. . . . . . . . . . . . . . . . . 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 3523	. . . . . . . . . . . . . . . . . . . . 21 |- { x e. ( B ^m A ) | x finSupp Z } C_ ( B ^m A )
132	1, 131	eqsstri 3471	. . . . . . . . . . . . . . . . . . . 20 |- U C_ ( B ^m A )
133	132, 116	sseldi 3439	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
134		elmapi 7477	. . . . . . . . . . . . . . . . . . 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 7988	. . . . . . . . . . . . . . . . . . 19 |- F : dom F --> A
137	136	ffvelrni 6007	. . . . . . . . . . . . . . . . . 18 |- ( c e. dom F -> ( F ` c ) e. A )
138		ffvelrn 6006	. . . . . . . . . . . . . . . . . 18 |- ( ( x : A --> B /\ ( F ` c ) e. A ) -> ( x ` ( F ` c ) ) e. B )
139	135, 137, 138	syl2an 475	. . . . . . . . . . . . . . . . 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 3439	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
141		elmapi 7477	. . . . . . . . . . . . . . . . . . 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 6006	. . . . . . . . . . . . . . . . . 18 |- ( ( y : A --> B /\ ( F ` c ) e. A ) -> ( y ` ( F ` c ) ) e. B )
144	142, 137, 143	syl2an 475	. . . . . . . . . . . . . . . . 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 6204	. . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . 17 |- ( `' G ` ( y ` ( F ` c ) ) ) e. _V
148	147	epelc 4735	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> x : A --> B )
151		fco 5723	. . . . . . . . . . . . . . . . . . 19 |- ( ( x : A --> B /\ F : dom F --> A ) -> ( x o. F ) : dom F --> B )
152	150, 136, 151	sylancl 660	. . . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> c e. dom F )
156		fvco3 5925	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
157	136, 155, 156	sylancr 661	. . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> y : A --> B )
161		fco 5723	. . . . . . . . . . . . . . . . . . 19 |- ( ( y : A --> B /\ F : dom F --> A ) -> ( y o. F ) : dom F --> B )
162	160, 136, 161	sylancl 660	. . . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
166	136, 155, 165	sylancr 661	. . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . 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 2484	. . . . . . . . . . . . . . 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 3009	. . . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
173		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
174		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
175	173, 174	eqeq12d 2424	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( x ` w ) = ( y ` w ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
176	172, 175	imbi12d 318	. . . . . . . . . . . . . . . . . . 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 6011	. . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 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 4736	. . . . . . . . . . . . . . . . . . 19 |- ( c _E d <-> c e. d )
182	9	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 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 6204	. . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . 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 2424	. . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . 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 5797	. . . . . . . . . . . . . . . . . . . . 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 6009	. . . . . . . . . . . . . . . . . . . 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 6009	. . . . . . . . . . . . . . . . . . . 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 6150	. . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
202	136, 187, 201	sylancr 661	. . . . . . . . . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
204	136, 187, 203	sylancr 661	. . . . . . . . . . . . . . . . . . . 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 2424	. . . . . . . . . . . . . . . . . . 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 318	. . . . . . . . . . . . . . . . 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 646	. . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . 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 2914	. . . . . . . . . . . 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 432	. . . . . . . . 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 638	. . . . . . . 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 4457	. . . . . . 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 4828	. . . . . . . . 9 |- ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
220	218, 219	ineq12i 3638	. . . . . . . 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 4953	. . . . . . . 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 2431	. . . . . . 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 3637	. . . . . . . 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 4953	. . . . . . . 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 2431	. . . . . . 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 2468	. . . . . 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 4810	. . . . . 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 232	. . . 4 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) We U )
230		weinxp 4890	. . . 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 432	. 2 |- ( ph -> ( ( B e. _V /\ A e. _V ) -> T We U ) )
233		we0 4817	. . 3 |- T We (/)
234		elmapex 7476	. . . . . . . . 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 2815	. . . . . 6 |- ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
238		rabeq0 3760	. . . . . 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 2455	. . . 4 |- ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
241		weeq2 4811	. . . 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 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 367   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2753   E.wrex 2754   {crab 2757   _Vcvv 3058   i^i cin 3412   (/)c0 3737   class class class wbr 4394   {copab 4451   |-> cmpt 4452   _E cep 4731   We wwe 4780   X. cxp 4820   `'ccnv 4821   dom cdm 4822   ran crn 4823   o. ccom 4826   Ord word 5408   Oncon0 5409   Fn wfn 5563   -->wf 5564   -1-1->wf1 5565   -onto->wfo 5566   -1-1-onto->wf1o 5567   ` cfv 5568   Isom wiso 5569  (class class class)co 6277   ^o coe 7165   ^m cmap 7456   finSupp cfsupp 7862  OrdIsocoi 7967   CNF ccnf 8109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6683  df-1st 6783  df-2nd 6784  df-supp 6902  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-seqom 7149  df-1o 7166  df-2o 7167  df-oadd 7170  df-omul 7171  df-oexp 7172  df-er 7347  df-map 7458  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-fsupp 7863  df-oi 7968  df-cnf 8110

This theorem is referenced by:  ltbwe  18455