Theorem wemapwe 8594

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 2622	. . . . . . . . 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 2622	. . . . . . . . 9 |- ( `' G ` Z ) = ( `' G ` Z )
4		simprr 796	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> A e. _V )
5		wemapwe.2	. . . . . . . . . . . 12 |- ( ph -> R We A )
6	5	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> R We A )
7		wemapwe.5	. . . . . . . . . . . 12 |- F = OrdIso ( R , A )
8	7	oiiso 8442	. . . . . . . . . . 11 |- ( ( A e. _V /\ R We A ) -> F Isom _E , R ( dom F , A ) )
9	4, 6, 8	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F Isom _E , R ( dom F , A ) )
10		isof1o 6573	. . . . . . . . . 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 794	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B e. _V )
13		wemapwe.3	. . . . . . . . . . . 12 |- ( ph -> S We B )
14	13	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> S We B )
15		wemapwe.6	. . . . . . . . . . . 12 |- G = OrdIso ( S , B )
16	15	oiiso 8442	. . . . . . . . . . 11 |- ( ( B e. _V /\ S We B ) -> G Isom _E , S ( dom G , B ) )
17	12, 14, 16	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G Isom _E , S ( dom G , B ) )
18		isof1o 6573	. . . . . . . . . 10 |- ( G Isom _E , S ( dom G , B ) -> G : dom G -1-1-onto-> B )
19		f1ocnv 6149	. . . . . . . . . 10 |- ( G : dom G -1-1-onto-> B -> `' G : B -1-1-onto-> dom G )
20	17, 18, 19	3syl 18	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> `' G : B -1-1-onto-> dom G )
21	7	oiexg 8440	. . . . . . . . . . 11 |- ( A e. _V -> F e. _V )
22	21	ad2antll 765	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F e. _V )
23		dmexg 7097	. . . . . . . . . 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 8440	. . . . . . . . . . 11 |- ( B e. _V -> G e. _V )
26	25	ad2antrl 764	. . . . . . . . . 10 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G e. _V )
27		dmexg 7097	. . . . . . . . . 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 6144	. . . . . . . . . . . . . . 15 |- ( G : dom G -1-1-onto-> B -> G : dom G -onto-> B )
32		forn 6118	. . . . . . . . . . . . . . 15 |- ( G : dom G -onto-> B -> ran G = B )
33	30, 31, 32	3syl 18	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G = B )
34		wemapwe.4	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= (/) )
35	34	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B =/= (/) )
36	33, 35	eqnetrd 2861	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G =/= (/) )
37		dm0rn0 5342	. . . . . . . . . . . . . 14 |- ( dom G = (/) <-> ran G = (/) )
38	37	necon3bii 2846	. . . . . . . . . . . . 13 |- ( dom G =/= (/) <-> ran G =/= (/) )
39	36, 38	sylibr 224	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G =/= (/) )
40	15	oicl 8434	. . . . . . . . . . . . 13 |- Ord dom G
41		ord0eln0 5779	. . . . . . . . . . . . 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 224	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> (/) e. dom G )
44	15	oif 8435	. . . . . . . . . . . 12 |- G : dom G --> B
45	44	ffvelrni 6358	. . . . . . . . . . 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 2705	. . . . . . . . 9 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> Z e. B )
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 8313	. . . . . . . 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 2622	. . . . . . . . . . 11 |- { x e. ( dom G ^m dom F ) | x finSupp (/) } = { x e. ( dom G ^m dom F ) | x finSupp (/) }
50	15	oion 8441	. . . . . . . . . . . 12 |- ( B e. _V -> dom G e. On )
51	50	ad2antrl 764	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. On )
52	7	oion 8441	. . . . . . . . . . . 12 |- ( A e. _V -> dom F e. On )
53	52	ad2antll 765	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. On )
54	49, 51, 53	cantnfdm 8561	. . . . . . . . . 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 6194	. . . . . . . . . . . . 13 |- ( `' G ` Z ) = ( `' G ` ( G ` (/) ) )
56		f1ocnvfv1 6532	. . . . . . . . . . . . . 14 |- ( ( G : dom G -1-1-onto-> B /\ (/) e. dom G ) -> ( `' G ` ( G ` (/) ) ) = (/) )
57	30, 43, 56	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` ( G ` (/) ) ) = (/) )
58	55, 57	syl5eq 2668	. . . . . . . . . . . 12 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` Z ) = (/) )
59	58	breq2d 4665	. . . . . . . . . . 11 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( x finSupp ( `' G ` Z ) <-> x finSupp (/) ) )
60	59	rabbidv 3189	. . . . . . . . . 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 2659	. . . . . . . . 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 6129	. . . . . . . . 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 247	. . . . . . 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 2622	. . . . . . . . 9 |- dom ( dom G CNF dom F ) = dom ( dom G CNF dom F )
66		eqid 2622	. . . . . . . . 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 8591	. . . . . . . 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 475	. . . . . . 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 2622	. . . . . . . 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 6603	. . . . . . 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 65	. . . . . 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 5186	. . . . . 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 208	. . . . 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 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F : dom F -1-1-onto-> A )
75		f1ofn 6138	. . . . . . . . . . . 12 |- ( F : dom F -1-1-onto-> A -> F Fn dom F )
76		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
77		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
78	76, 77	breq12d 4666	. . . . . . . . . . . . . 14 |- ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
79		breq1 4656	. . . . . . . . . . . . . . . 16 |- ( z = ( F ` c ) -> ( z R w <-> ( F ` c ) R w ) )
80	79	imbi1d 331	. . . . . . . . . . . . . . 15 |- ( z = ( F ` c ) -> ( ( z R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
81	80	ralbidv 2986	. . . . . . . . . . . . . 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 747	. . . . . . . . . . . . 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 6361	. . . . . . . . . . . 12 |- ( F Fn dom F -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
84	74, 75, 83	3syl 18	. . . . . . . . . . 11 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
85		f1ofo 6144	. . . . . . . . . . . . 13 |- ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
86		forn 6118	. . . . . . . . . . . . 13 |- ( F : dom F -onto-> A -> ran F = A )
87	74, 85, 86	3syl 18	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ran F = A )
88	87	rexeqdv 3145	. . . . . . . . . . 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 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> G e. _V )
90		cnvexg 7112	. . . . . . . . . . . . . . 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 3203	. . . . . . . . . . . . . . 15 |- x e. _V
93	22	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F e. _V )
94		coexg 7117	. . . . . . . . . . . . . . 15 |- ( ( x e. _V /\ F e. _V ) -> ( x o. F ) e. _V )
95	92, 93, 94	sylancr 695	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( x o. F ) e. _V )
96		coexg 7117	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( x o. F ) e. _V ) -> ( `' G o. ( x o. F ) ) e. _V )
97	91, 95, 96	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( x o. F ) ) e. _V )
98		vex 3203	. . . . . . . . . . . . . . 15 |- y e. _V
99		coexg 7117	. . . . . . . . . . . . . . 15 |- ( ( y e. _V /\ F e. _V ) -> ( y o. F ) e. _V )
100	98, 93, 99	sylancr 695	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( y o. F ) e. _V )
101		coexg 7117	. . . . . . . . . . . . . 14 |- ( ( `' G e. _V /\ ( y o. F ) e. _V ) -> ( `' G o. ( y o. F ) ) e. _V )
102	91, 100, 101	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( y o. F ) ) e. _V )
103		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
104		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
105		eleq12 2691	. . . . . . . . . . . . . . . . 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 494	. . . . . . . . . . . . . . . 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 6190	. . . . . . . . . . . . . . . . . . 19 |- ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
108		fveq1 6190	. . . . . . . . . . . . . . . . . . 19 |- ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
109	107, 108	eqeqan12d 2638	. . . . . . . . . . . . . . . . . 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 330	. . . . . . . . . . . . . . . . 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 2986	. . . . . . . . . . . . . . . 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 747	. . . . . . . . . . . . . . 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 3052	. . . . . . . . . . . . . 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 4989	. . . . . . . . . . . . 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 693	. . . . . . . . . . . 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 794	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. U )
117		coeq1 5279	. . . . . . . . . . . . . . . 16 |- ( f = x -> ( f o. F ) = ( x o. F ) )
118	117	coeq2d 5284	. . . . . . . . . . . . . . 15 |- ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
119		eqid 2622	. . . . . . . . . . . . . . 15 |- ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
120	118, 119	fvmptg 6280	. . . . . . . . . . . . . 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 693	. . . . . . . . . . . . 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 796	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
123		coeq1 5279	. . . . . . . . . . . . . . . 16 |- ( f = y -> ( f o. F ) = ( y o. F ) )
124	123	coeq2d 5284	. . . . . . . . . . . . . . 15 |- ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
125	124, 119	fvmptg 6280	. . . . . . . . . . . . . 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 693	. . . . . . . . . . . . 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 4666	. . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . 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 6580	. . . . . . . . . . . . . . . . . 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 3687	. . . . . . . . . . . . . . . . . . . . 21 |- { x e. ( B ^m A ) | x finSupp Z } C_ ( B ^m A )
132	1, 131	eqsstri 3635	. . . . . . . . . . . . . . . . . . . 20 |- U C_ ( B ^m A )
133	132, 116	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
134		elmapi 7879	. . . . . . . . . . . . . . . . . . 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 8435	. . . . . . . . . . . . . . . . . . 19 |- F : dom F --> A
137	136	ffvelrni 6358	. . . . . . . . . . . . . . . . . 18 |- ( c e. dom F -> ( F ` c ) e. A )
138		ffvelrn 6357	. . . . . . . . . . . . . . . . . 18 |- ( ( x : A --> B /\ ( F ` c ) e. A ) -> ( x ` ( F ` c ) ) e. B )
139	135, 137, 138	syl2an 494	. . . . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
141		elmapi 7879	. . . . . . . . . . . . . . . . . . 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 6357	. . . . . . . . . . . . . . . . . 18 |- ( ( y : A --> B /\ ( F ` c ) e. A ) -> ( y ` ( F ` c ) ) e. B )
144	142, 137, 143	syl2an 494	. . . . . . . . . . . . . . . . 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 6576	. . . . . . . . . . . . . . . . 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 1324	. . . . . . . . . . . . . . . 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 6201	. . . . . . . . . . . . . . . . 17 |- ( `' G ` ( y ` ( F ` c ) ) ) e. _V
148	147	epelc 5031	. . . . . . . . . . . . . . . 16 |- ( ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) )
149	146, 148	syl6bb 276	. . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> x : A --> B )
151		fco 6058	. . . . . . . . . . . . . . . . . . 19 |- ( ( x : A --> B /\ F : dom F --> A ) -> ( x o. F ) : dom F --> B )
152	150, 136, 151	sylancl 694	. . . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . 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 701	. . . . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> c e. dom F )
156		fvco3 6275	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
157	136, 155, 156	sylancr 695	. . . . . . . . . . . . . . . . . 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 6195	. . . . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> y : A --> B )
161		fco 6058	. . . . . . . . . . . . . . . . . . 19 |- ( ( y : A --> B /\ F : dom F --> A ) -> ( y o. F ) : dom F --> B )
162	160, 136, 161	sylancl 694	. . . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . 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 701	. . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : dom F --> A /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
166	136, 155, 165	sylancr 695	. . . . . . . . . . . . . . . . . 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 6195	. . . . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . . . 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 2695	. . . . . . . . . . . . . . 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 271	. . . . . . . . . . . . . 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 3144	. . . . . . . . . . . . . . . . 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 4657	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
173		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
174		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
175	173, 174	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( F ` d ) -> ( ( x ` w ) = ( y ` w ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
176	172, 175	imbi12d 334	. . . . . . . . . . . . . . . . . . 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 6362	. . . . . . . . . . . . . . . . . 18 |- ( F Fn dom F -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
178	74, 75, 177	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
179	171, 178	bitr3d 270	. . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . 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 5032	. . . . . . . . . . . . . . . . . . 19 |- ( c _E d <-> c e. d )
182	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 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 6576	. . . . . . . . . . . . . . . . . . . 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 701	. . . . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . . 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 753	. . . . . . . . . . . . . . . . . . . . 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 796	. . . . . . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . 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 753	. . . . . . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . 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 2637	. . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . 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 6136	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' G : B -1-1-onto-> dom G -> `' G : B -1-1-> dom G )
196	194, 19, 195	3syl 18	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> `' G : B -1-1-> dom G )
197	186, 187	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 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 6360	. . . . . . . . . . . . . . . . . . . 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 6519	. . . . . . . . . . . . . . . . . . . 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 1324	. . . . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
202	136, 187, 201	sylancr 695	. . . . . . . . . . . . . . . . . . . 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 6275	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : dom F --> A /\ d e. dom F ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
204	136, 187, 203	sylancr 695	. . . . . . . . . . . . . . . . . . . 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 2637	. . . . . . . . . . . . . . . . . . 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 294	. . . . . . . . . . . . . . . . . 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 334	. . . . . . . . . . . . . . . . 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 680	. . . . . . . . . . . . . . . 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 2985	. . . . . . . . . . . . . . 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 271	. . . . . . . . . . . . . 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 747	. . . . . . . . . . . . 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 3049	. . . . . . . . . . . 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 301	. . . . . . . . . . 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 298	. . . . . . . . . 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 450	. . . . . . . . 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 672	. . . . . . . 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 4716	. . . . . . 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 5120	. . . . . . . . 9 |- ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
220	218, 219	ineq12i 3812	. . . . . . . 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 5252	. . . . . . . 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 2644	. . . . . . 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 3811	. . . . . . . 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 5252	. . . . . . . 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 2644	. . . . . . 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 2681	. . . . . 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 5102	. . . . . 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 247	. . . 4 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) We U )
230		weinxp 5186	. . . 4 |- ( T We U <-> ( T i^i ( U X. U ) ) We U )
231	229, 230	sylibr 224	. . 3 |- ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> T We U )
232	231	ex 450	. 2 |- ( ph -> ( ( B e. _V /\ A e. _V ) -> T We U ) )
233		we0 5109	. . 3 |- T We (/)
234		elmapex 7878	. . . . . . . . 9 |- ( x e. ( B ^m A ) -> ( B e. _V /\ A e. _V ) )
235	234	con3i 150	. . . . . . . 8 |- ( -. ( B e. _V /\ A e. _V ) -> -. x e. ( B ^m A ) )
236	235	pm2.21d 118	. . . . . . 7 |- ( -. ( B e. _V /\ A e. _V ) -> ( x e. ( B ^m A ) -> -. x finSupp Z ) )
237	236	ralrimiv 2965	. . . . . 6 |- ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
238		rabeq0 3957	. . . . . 6 |- ( { x e. ( B ^m A ) | x finSupp Z } = (/) <-> A. x e. ( B ^m A ) -. x finSupp Z )
239	237, 238	sylibr 224	. . . . 5 |- ( -. ( B e. _V /\ A e. _V ) -> { x e. ( B ^m A ) | x finSupp Z } = (/) )
240	1, 239	syl5eq 2668	. . . 4 |- ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
241		weeq2 5103	. . . 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 248	. 2 |- ( -. ( B e. _V /\ A e. _V ) -> T We U )
244	232, 243	pm2.61d1 171	1 |- ( ph -> T We U )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   i^i cin 3573   (/)c0 3915   class class class wbr 4653   {copab 4712   |-> cmpt 4729   _E cep 5028   We wwe 5072   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   o. ccom 5118   Ord word 5722   Oncon0 5723   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889  (class class class)co 6650   ^o coe 7559   ^m cmap 7857   finSupp cfsupp 8275  OrdIsocoi 8414   CNF ccnf 8558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seqom 7543  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-oexp 7566  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-cnf 8559

This theorem is referenced by:  ltbwe  19472