Theorem iundom2g 9362

Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ). (Contributed by Mario Carneiro, 1-Sep-2015.)

Hypotheses

Ref	Expression
iunfo.1	|- T = U_ x e. A ( { x } X. B )
iundomg.2	|- ( ph -> U_ x e. A ( C ^m B ) e. AC A )
iundomg.3	|- ( ph -> A. x e. A B ~<_ C )

Assertion

Ref	Expression
iundom2g	|- ( ph -> T ~<_ ( A X. C ) )

Distinct variable groups:   x, A   x, C

Allowed substitution hints:   ph( x)   B( x)   T( x)

Proof of Theorem iundom2g

Dummy variables f g y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iundomg.2	. . 3 |- ( ph -> U_ x e. A ( C ^m B ) e. AC A )
2		iundomg.3	. . . . 5 |- ( ph -> A. x e. A B ~<_ C )
3		brdomi 7966	. . . . . . . . 9 |- ( B ~<_ C -> E. g g : B -1-1-> C )
4	3	adantl 482	. . . . . . . 8 |- ( ( x e. A /\ B ~<_ C ) -> E. g g : B -1-1-> C )
5		f1f 6101	. . . . . . . . . . . 12 |- ( g : B -1-1-> C -> g : B --> C )
6		reldom 7961	. . . . . . . . . . . . . . 15 |- Rel ~<_
7	6	brrelex2i 5159	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> C e. _V )
8	6	brrelexi 5158	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> B e. _V )
9	7, 8	elmapd 7871	. . . . . . . . . . . . 13 |- ( B ~<_ C -> ( g e. ( C ^m B ) <-> g : B --> C ) )
10	9	adantl 482	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
11	5, 10	syl5ibr 236	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. ( C ^m B ) ) )
12		ssiun2 4563	. . . . . . . . . . . . 13 |- ( x e. A -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
13	12	adantr 481	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
14	13	sseld 3602	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) -> g e. U_ x e. A ( C ^m B ) ) )
15	11, 14	syld 47	. . . . . . . . . 10 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. U_ x e. A ( C ^m B ) ) )
16	15	ancrd 577	. . . . . . . . 9 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> ( g e. U_ x e. A ( C ^m B ) /\ g : B -1-1-> C ) ) )
17	16	eximdv 1846	. . . . . . . 8 |- ( ( x e. A /\ B ~<_ C ) -> ( E. g g : B -1-1-> C -> E. g ( g e. U_ x e. A ( C ^m B ) /\ g : B -1-1-> C ) ) )
18	4, 17	mpd 15	. . . . . . 7 |- ( ( x e. A /\ B ~<_ C ) -> E. g ( g e. U_ x e. A ( C ^m B ) /\ g : B -1-1-> C ) )
19		df-rex 2918	. . . . . . 7 |- ( E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C <-> E. g ( g e. U_ x e. A ( C ^m B ) /\ g : B -1-1-> C ) )
20	18, 19	sylibr 224	. . . . . 6 |- ( ( x e. A /\ B ~<_ C ) -> E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
21	20	ralimiaa 2951	. . . . 5 |- ( A. x e. A B ~<_ C -> A. x e. A E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
22	2, 21	syl 17	. . . 4 |- ( ph -> A. x e. A E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
23		nfv 1843	. . . . 5 |- F/ y E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C
24		nfiu1 4550	. . . . . 6 |- F/_ x U_ x e. A ( C ^m B )
25		nfcv 2764	. . . . . . 7 |- F/_ x g
26		nfcsb1v 3549	. . . . . . 7 |- F/_ x [_ y / x ]_ B
27		nfcv 2764	. . . . . . 7 |- F/_ x C
28	25, 26, 27	nff1 6099	. . . . . 6 |- F/ x g : [_ y / x ]_ B -1-1-> C
29	24, 28	nfrex 3007	. . . . 5 |- F/ x E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C
30		csbeq1a 3542	. . . . . . 7 |- ( x = y -> B = [_ y / x ]_ B )
31		f1eq2 6097	. . . . . . 7 |- ( B = [_ y / x ]_ B -> ( g : B -1-1-> C <-> g : [_ y / x ]_ B -1-1-> C ) )
32	30, 31	syl 17	. . . . . 6 |- ( x = y -> ( g : B -1-1-> C <-> g : [_ y / x ]_ B -1-1-> C ) )
33	32	rexbidv 3052	. . . . 5 |- ( x = y -> ( E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C <-> E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C ) )
34	23, 29, 33	cbvral 3167	. . . 4 |- ( A. x e. A E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C <-> A. y e. A E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C )
35	22, 34	sylib 208	. . 3 |- ( ph -> A. y e. A E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C )
36		f1eq1 6096	. . . 4 |- ( g = ( f ` y ) -> ( g : [_ y / x ]_ B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
37	36	acni3 8870	. . 3 |- ( ( U_ x e. A ( C ^m B ) e. AC A /\ A. y e. A E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C ) -> E. f ( f : A --> U_ x e. A ( C ^m B ) /\ A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
38	1, 35, 37	syl2anc 693	. 2 |- ( ph -> E. f ( f : A --> U_ x e. A ( C ^m B ) /\ A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
39		nfv 1843	. . . . . 6 |- F/ y ( f ` x ) : B -1-1-> C
40		nfcv 2764	. . . . . . 7 |- F/_ x ( f ` y )
41	40, 26, 27	nff1 6099	. . . . . 6 |- F/ x ( f ` y ) : [_ y / x ]_ B -1-1-> C
42		fveq2 6191	. . . . . . . 8 |- ( x = y -> ( f ` x ) = ( f ` y ) )
43		f1eq1 6096	. . . . . . . 8 |- ( ( f ` x ) = ( f ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : B -1-1-> C ) )
44	42, 43	syl 17	. . . . . . 7 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : B -1-1-> C ) )
45		f1eq2 6097	. . . . . . . 8 |- ( B = [_ y / x ]_ B -> ( ( f ` y ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
46	30, 45	syl 17	. . . . . . 7 |- ( x = y -> ( ( f ` y ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
47	44, 46	bitrd 268	. . . . . 6 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
48	39, 41, 47	cbvral 3167	. . . . 5 |- ( A. x e. A ( f ` x ) : B -1-1-> C <-> A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C )
49		df-ne 2795	. . . . . . . 8 |- ( A =/= (/) <-> -. A = (/) )
50		acnrcl 8865	. . . . . . . . . 10 |- ( U_ x e. A ( C ^m B ) e. AC A -> A e. _V )
51	1, 50	syl 17	. . . . . . . . 9 |- ( ph -> A e. _V )
52		r19.2z 4060	. . . . . . . . . . . 12 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> E. x e. A B ~<_ C )
53	7	rexlimivw 3029	. . . . . . . . . . . 12 |- ( E. x e. A B ~<_ C -> C e. _V )
54	52, 53	syl 17	. . . . . . . . . . 11 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> C e. _V )
55	54	expcom 451	. . . . . . . . . 10 |- ( A. x e. A B ~<_ C -> ( A =/= (/) -> C e. _V ) )
56	2, 55	syl 17	. . . . . . . . 9 |- ( ph -> ( A =/= (/) -> C e. _V ) )
57		xpexg 6960	. . . . . . . . 9 |- ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
58	51, 56, 57	syl6an 568	. . . . . . . 8 |- ( ph -> ( A =/= (/) -> ( A X. C ) e. _V ) )
59	49, 58	syl5bir 233	. . . . . . 7 |- ( ph -> ( -. A = (/) -> ( A X. C ) e. _V ) )
60		xpeq1 5128	. . . . . . . 8 |- ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
61		0xp 5199	. . . . . . . . 9 |- ( (/) X. C ) = (/)
62		0ex 4790	. . . . . . . . 9 |- (/) e. _V
63	61, 62	eqeltri 2697	. . . . . . . 8 |- ( (/) X. C ) e. _V
64	60, 63	syl6eqel 2709	. . . . . . 7 |- ( A = (/) -> ( A X. C ) e. _V )
65	59, 64	pm2.61d2 172	. . . . . 6 |- ( ph -> ( A X. C ) e. _V )
66		iunfo.1	. . . . . . . . . 10 |- T = U_ x e. A ( { x } X. B )
67	66	eleq2i 2693	. . . . . . . . 9 |- ( y e. T <-> y e. U_ x e. A ( { x } X. B ) )
68		eliun 4524	. . . . . . . . 9 |- ( y e. U_ x e. A ( { x } X. B ) <-> E. x e. A y e. ( { x } X. B ) )
69	67, 68	bitri 264	. . . . . . . 8 |- ( y e. T <-> E. x e. A y e. ( { x } X. B ) )
70		r19.29 3072	. . . . . . . . . 10 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ E. x e. A y e. ( { x } X. B ) ) -> E. x e. A ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) )
71		xp1st 7198	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 1st ` y ) e. { x } )
72	71	ad2antll 765	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. { x } )
73		elsni 4194	. . . . . . . . . . . . . 14 |- ( ( 1st ` y ) e. { x } -> ( 1st ` y ) = x )
74	72, 73	syl 17	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) = x )
75		simpl 473	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x e. A )
76	74, 75	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. A )
77	74	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` ( 1st ` y ) ) = ( f ` x ) )
78	77	fveq1d 6193	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` x ) ` ( 2nd ` y ) ) )
79		f1f 6101	. . . . . . . . . . . . . . 15 |- ( ( f ` x ) : B -1-1-> C -> ( f ` x ) : B --> C )
80	79	ad2antrl 764	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` x ) : B --> C )
81		xp2nd 7199	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 2nd ` y ) e. B )
82	81	ad2antll 765	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. B )
83	80, 82	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` x ) ` ( 2nd ` y ) ) e. C )
84	78, 83	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C )
85		opelxpi 5148	. . . . . . . . . . . 12 |- ( ( ( 1st ` y ) e. A /\ ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C ) -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) )
86	76, 84, 85	syl2anc 693	. . . . . . . . . . 11 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) )
87	86	rexlimiva 3028	. . . . . . . . . 10 |- ( E. x e. A ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) )
88	70, 87	syl 17	. . . . . . . . 9 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ E. x e. A y e. ( { x } X. B ) ) -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) )
89	88	ex 450	. . . . . . . 8 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( E. x e. A y e. ( { x } X. B ) -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) ) )
90	69, 89	syl5bi 232	. . . . . . 7 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) ) )
91		fvex 6201	. . . . . . . . . 10 |- ( 1st ` y ) e. _V
92		fvex 6201	. . . . . . . . . 10 |- ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. _V
93	91, 92	opth 4945	. . . . . . . . 9 |- ( <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. = <. ( 1st ` z ) , ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) >. <-> ( ( 1st ` y ) = ( 1st ` z ) /\ ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) )
94		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 1st ` y ) = ( 1st ` z ) )
95	94	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( f ` ( 1st ` y ) ) = ( f ` ( 1st ` z ) ) )
96	95	fveq1d 6193	. . . . . . . . . . . . 13 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` z ) ) = ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) )
97	96	eqeq2d 2632	. . . . . . . . . . . 12 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` y ) ) ` ( 2nd ` z ) ) <-> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) )
98		djussxp 5267	. . . . . . . . . . . . . . . . . 18 |- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
99	66, 98	eqsstri 3635	. . . . . . . . . . . . . . . . 17 |- T C_ ( A X. _V )
100		simprl 794	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. T )
101	99, 100	sseldi 3601	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. ( A X. _V ) )
102	101	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> y e. ( A X. _V ) )
103		xp1st 7198	. . . . . . . . . . . . . . 15 |- ( y e. ( A X. _V ) -> ( 1st ` y ) e. A )
104	102, 103	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 1st ` y ) e. A )
105		simpll 790	. . . . . . . . . . . . . 14 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> A. x e. A ( f ` x ) : B -1-1-> C )
106		nfcv 2764	. . . . . . . . . . . . . . . 16 |- F/_ x ( f ` ( 1st ` y ) )
107		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 |- F/_ x [_ ( 1st ` y ) / x ]_ B
108	106, 107, 27	nff1 6099	. . . . . . . . . . . . . . 15 |- F/ x ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C
109		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> ( f ` x ) = ( f ` ( 1st ` y ) ) )
110		f1eq1 6096	. . . . . . . . . . . . . . . . 17 |- ( ( f ` x ) = ( f ` ( 1st ` y ) ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : B -1-1-> C ) )
111	109, 110	syl 17	. . . . . . . . . . . . . . . 16 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : B -1-1-> C ) )
112		csbeq1a 3542	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> B = [_ ( 1st ` y ) / x ]_ B )
113		f1eq2 6097	. . . . . . . . . . . . . . . . 17 |- ( B = [_ ( 1st ` y ) / x ]_ B -> ( ( f ` ( 1st ` y ) ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
114	112, 113	syl 17	. . . . . . . . . . . . . . . 16 |- ( x = ( 1st ` y ) -> ( ( f ` ( 1st ` y ) ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
115	111, 114	bitrd 268	. . . . . . . . . . . . . . 15 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
116	108, 115	rspc 3303	. . . . . . . . . . . . . 14 |- ( ( 1st ` y ) e. A -> ( A. x e. A ( f ` x ) : B -1-1-> C -> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
117	104, 105, 116	sylc 65	. . . . . . . . . . . . 13 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C )
118	107	nfel2 2781	. . . . . . . . . . . . . . . . . . . 20 |- F/ x ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B
119	74	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x = ( 1st ` y ) )
120	119, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> B = [_ ( 1st ` y ) / x ]_ B )
121	82, 120	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
122	121	ex 450	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. A -> ( ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
123	118, 122	rexlimi 3024	. . . . . . . . . . . . . . . . . . 19 |- ( E. x e. A ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
124	70, 123	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ E. x e. A y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
125	124	ex 450	. . . . . . . . . . . . . . . . 17 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( E. x e. A y e. ( { x } X. B ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
126	69, 125	syl5bi 232	. . . . . . . . . . . . . . . 16 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
127	126	imp 445	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ y e. T ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
128	127	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
129	128	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
130	126	ralrimiv 2965	. . . . . . . . . . . . . . . . 17 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
131		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( 2nd ` y ) = ( 2nd ` z ) )
132		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( y = z -> ( 1st ` y ) = ( 1st ` z ) )
133	132	csbeq1d 3540	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
134	131, 133	eleq12d 2695	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B <-> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B ) )
135	134	rspccva 3308	. . . . . . . . . . . . . . . . 17 |- ( ( A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
136	130, 135	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
137	136	adantrl 752	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
138	137	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
139	94	csbeq1d 3540	. . . . . . . . . . . . . 14 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
140	138, 139	eleqtrrd 2704	. . . . . . . . . . . . 13 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 2nd ` z ) e. [_ ( 1st ` y ) / x ]_ B )
141		f1fveq 6519	. . . . . . . . . . . . 13 |- ( ( ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C /\ ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B /\ ( 2nd ` z ) e. [_ ( 1st ` y ) / x ]_ B ) ) -> ( ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` y ) ) ` ( 2nd ` z ) ) <-> ( 2nd ` y ) = ( 2nd ` z ) ) )
142	117, 129, 140, 141	syl12anc 1324	. . . . . . . . . . . 12 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` y ) ) ` ( 2nd ` z ) ) <-> ( 2nd ` y ) = ( 2nd ` z ) ) )
143	97, 142	bitr3d 270	. . . . . . . . . . 11 |- ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) <-> ( 2nd ` y ) = ( 2nd ` z ) ) )
144	143	pm5.32da 673	. . . . . . . . . 10 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( ( ( 1st ` y ) = ( 1st ` z ) /\ ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) <-> ( ( 1st ` y ) = ( 1st ` z ) /\ ( 2nd ` y ) = ( 2nd ` z ) ) ) )
145		simprr 796	. . . . . . . . . . . 12 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. T )
146	99, 145	sseldi 3601	. . . . . . . . . . 11 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. ( A X. _V ) )
147		xpopth 7207	. . . . . . . . . . 11 |- ( ( y e. ( A X. _V ) /\ z e. ( A X. _V ) ) -> ( ( ( 1st ` y ) = ( 1st ` z ) /\ ( 2nd ` y ) = ( 2nd ` z ) ) <-> y = z ) )
148	101, 146, 147	syl2anc 693	. . . . . . . . . 10 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( ( ( 1st ` y ) = ( 1st ` z ) /\ ( 2nd ` y ) = ( 2nd ` z ) ) <-> y = z ) )
149	144, 148	bitrd 268	. . . . . . . . 9 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( ( ( 1st ` y ) = ( 1st ` z ) /\ ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) <-> y = z ) )
150	93, 149	syl5bb 272	. . . . . . . 8 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. = <. ( 1st ` z ) , ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) >. <-> y = z ) )
151	150	ex 450	. . . . . . 7 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( ( y e. T /\ z e. T ) -> ( <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. = <. ( 1st ` z ) , ( ( f ` ( 1st ` z ) ) ` ( 2nd ` z ) ) >. <-> y = z ) ) )
152	90, 151	dom2d 7996	. . . . . 6 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( ( A X. C ) e. _V -> T ~<_ ( A X. C ) ) )
153	65, 152	syl5com 31	. . . . 5 |- ( ph -> ( A. x e. A ( f ` x ) : B -1-1-> C -> T ~<_ ( A X. C ) ) )
154	48, 153	syl5bir 233	. . . 4 |- ( ph -> ( A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C -> T ~<_ ( A X. C ) ) )
155	154	adantld 483	. . 3 |- ( ph -> ( ( f : A --> U_ x e. A ( C ^m B ) /\ A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C ) -> T ~<_ ( A X. C ) ) )
156	155	exlimdv 1861	. 2 |- ( ph -> ( E. f ( f : A --> U_ x e. A ( C ^m B ) /\ A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C ) -> T ~<_ ( A X. C ) ) )
157	38, 156	mpd 15	1 |- ( ph -> T ~<_ ( A X. C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   [_csb 3533   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   X. cxp 5112   -->wf 5884   -1-1->wf1 5885   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   ~<_ cdom 7953  AC wacn 8764

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-3an 1039  df-tru 1486  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-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  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-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859  df-dom 7957  df-acn 8768

This theorem is referenced by:  iundomg  9363  iundom  9364