Theorem iundom2g 8972

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 7591	. . . . . . . . 9 |- ( B ~<_ C -> E. g g : B -1-1-> C )
4	3	adantl 467	. . . . . . . 8 |- ( ( x e. A /\ B ~<_ C ) -> E. g g : B -1-1-> C )
5		f1f 5796	. . . . . . . . . . . 12 |- ( g : B -1-1-> C -> g : B --> C )
6		reldom 7586	. . . . . . . . . . . . . . 15 |- Rel ~<_
7	6	brrelex2i 4895	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> C e. _V )
8	6	brrelexi 4894	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> B e. _V )
9	7, 8	elmapd 7497	. . . . . . . . . . . . 13 |- ( B ~<_ C -> ( g e. ( C ^m B ) <-> g : B --> C ) )
10	9	adantl 467	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
11	5, 10	syl5ibr 224	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. ( C ^m B ) ) )
12		ssiun2 4342	. . . . . . . . . . . . 13 |- ( x e. A -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
13	12	adantr 466	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
14	13	sseld 3463	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) -> g e. U_ x e. A ( C ^m B ) ) )
15	11, 14	syld 45	. . . . . . . . . 10 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. U_ x e. A ( C ^m B ) ) )
16	15	ancrd 556	. . . . . . . . 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 1758	. . . . . . . 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 2777	. . . . . . 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 215	. . . . . 6 |- ( ( x e. A /\ B ~<_ C ) -> E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
21	20	ralimiaa 2814	. . . . 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 1755	. . . . 5 |- F/ y E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C
24		nfiu1 4329	. . . . . 6 |- F/_ x U_ x e. A ( C ^m B )
25		nfcv 2580	. . . . . . 7 |- F/_ x g
26		nfcsb1v 3411	. . . . . . 7 |- F/_ x [_ y / x ]_ B
27		nfcv 2580	. . . . . . 7 |- F/_ x C
28	25, 26, 27	nff1 5794	. . . . . 6 |- F/ x g : [_ y / x ]_ B -1-1-> C
29	24, 28	nfrex 2885	. . . . 5 |- F/ x E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C
30		csbeq1a 3404	. . . . . . 7 |- ( x = y -> B = [_ y / x ]_ B )
31		f1eq2 5792	. . . . . . 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 2936	. . . . 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 3050	. . . 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 199	. . 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 5791	. . . 4 |- ( g = ( f ` y ) -> ( g : [_ y / x ]_ B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
37	36	acni3 8485	. . 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 665	. 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 1755	. . . . . 6 |- F/ y ( f ` x ) : B -1-1-> C
40		nfcv 2580	. . . . . . 7 |- F/_ x ( f ` y )
41	40, 26, 27	nff1 5794	. . . . . 6 |- F/ x ( f ` y ) : [_ y / x ]_ B -1-1-> C
42		fveq2 5881	. . . . . . . 8 |- ( x = y -> ( f ` x ) = ( f ` y ) )
43		f1eq1 5791	. . . . . . . 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 5792	. . . . . . . 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 256	. . . . . 6 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
48	39, 41, 47	cbvral 3050	. . . . 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 2616	. . . . . . . 8 |- ( A =/= (/) <-> -. A = (/) )
50		acnrcl 8480	. . . . . . . . . 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 3888	. . . . . . . . . . . 12 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> E. x e. A B ~<_ C )
53	7	rexlimivw 2911	. . . . . . . . . . . 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 436	. . . . . . . . . 10 |- ( A. x e. A B ~<_ C -> ( A =/= (/) -> C e. _V ) )
56	2, 55	syl 17	. . . . . . . . 9 |- ( ph -> ( A =/= (/) -> C e. _V ) )
57		xpexg 6607	. . . . . . . . 9 |- ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
58	51, 56, 57	syl6an 547	. . . . . . . 8 |- ( ph -> ( A =/= (/) -> ( A X. C ) e. _V ) )
59	49, 58	syl5bir 221	. . . . . . 7 |- ( ph -> ( -. A = (/) -> ( A X. C ) e. _V ) )
60		xpeq1 4867	. . . . . . . 8 |- ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
61		0xp 4934	. . . . . . . . 9 |- ( (/) X. C ) = (/)
62		0ex 4556	. . . . . . . . 9 |- (/) e. _V
63	61, 62	eqeltri 2503	. . . . . . . 8 |- ( (/) X. C ) e. _V
64	60, 63	syl6eqel 2515	. . . . . . 7 |- ( A = (/) -> ( A X. C ) e. _V )
65	59, 64	pm2.61d2 163	. . . . . 6 |- ( ph -> ( A X. C ) e. _V )
66		iunfo.1	. . . . . . . . . 10 |- T = U_ x e. A ( { x } X. B )
67	66	eleq2i 2499	. . . . . . . . 9 |- ( y e. T <-> y e. U_ x e. A ( { x } X. B ) )
68		eliun 4304	. . . . . . . . 9 |- ( y e. U_ x e. A ( { x } X. B ) <-> E. x e. A y e. ( { x } X. B ) )
69	67, 68	bitri 252	. . . . . . . 8 |- ( y e. T <-> E. x e. A y e. ( { x } X. B ) )
70		r19.29 2960	. . . . . . . . . 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 6837	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 1st ` y ) e. { x } )
72	71	ad2antll 733	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. { x } )
73		elsni 4023	. . . . . . . . . . . . . 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 458	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x e. A )
76	74, 75	eqeltrd 2507	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. A )
77	74	fveq2d 5885	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` ( 1st ` y ) ) = ( f ` x ) )
78	77	fveq1d 5883	. . . . . . . . . . . . 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 5796	. . . . . . . . . . . . . . 15 |- ( ( f ` x ) : B -1-1-> C -> ( f ` x ) : B --> C )
80	79	ad2antrl 732	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` x ) : B --> C )
81		xp2nd 6838	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 2nd ` y ) e. B )
82	81	ad2antll 733	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. B )
83	80, 82	ffvelrnd 6038	. . . . . . . . . . . . 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 2507	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C )
85		opelxpi 4885	. . . . . . . . . . . 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 665	. . . . . . . . . . 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 2910	. . . . . . . . . 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 435	. . . . . . . 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 220	. . . . . . 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 5891	. . . . . . . . . 10 |- ( 1st ` y ) e. _V
92		fvex 5891	. . . . . . . . . 10 |- ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. _V
93	91, 92	opth 4695	. . . . . . . . 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 462	. . . . . . . . . . . . . . 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 5885	. . . . . . . . . . . . . 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 5883	. . . . . . . . . . . . 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 2436	. . . . . . . . . . . 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 4999	. . . . . . . . . . . . . . . . . 18 |- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
99	66, 98	eqsstri 3494	. . . . . . . . . . . . . . . . 17 |- T C_ ( A X. _V )
100		simprl 762	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. T )
101	99, 100	sseldi 3462	. . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . 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 6837	. . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . 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 2580	. . . . . . . . . . . . . . . 16 |- F/_ x ( f ` ( 1st ` y ) )
107		nfcsb1v 3411	. . . . . . . . . . . . . . . 16 |- F/_ x [_ ( 1st ` y ) / x ]_ B
108	106, 107, 27	nff1 5794	. . . . . . . . . . . . . . 15 |- F/ x ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C
109		fveq2 5881	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> ( f ` x ) = ( f ` ( 1st ` y ) ) )
110		f1eq1 5791	. . . . . . . . . . . . . . . . 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 3404	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> B = [_ ( 1st ` y ) / x ]_ B )
113		f1eq2 5792	. . . . . . . . . . . . . . . . 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 256	. . . . . . . . . . . . . . 15 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
116	108, 115	rspc 3176	. . . . . . . . . . . . . 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 62	. . . . . . . . . . . . 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 2598	. . . . . . . . . . . . . . . . . . . 20 |- F/ x ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B
119	74	eqcomd 2430	. . . . . . . . . . . . . . . . . . . . . . 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 2509	. . . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . . 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 2904	. . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . 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 220	. . . . . . . . . . . . . . . 16 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
127	126	imp 430	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ y e. T ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
128	127	adantrr 721	. . . . . . . . . . . . . 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 466	. . . . . . . . . . . . 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 2834	. . . . . . . . . . . . . . . . 17 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
131		fveq2 5881	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( 2nd ` y ) = ( 2nd ` z ) )
132		fveq2 5881	. . . . . . . . . . . . . . . . . . . 20 |- ( y = z -> ( 1st ` y ) = ( 1st ` z ) )
133	132	csbeq1d 3402	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
134	131, 133	eleq12d 2501	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B <-> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B ) )
135	134	rspccva 3181	. . . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
137	136	adantrl 720	. . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . 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 3402	. . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . 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 6178	. . . . . . . . . . . . 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 1262	. . . . . . . . . . . 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 258	. . . . . . . . . . 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 645	. . . . . . . . . 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 764	. . . . . . . . . . . 12 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. T )
146	99, 145	sseldi 3462	. . . . . . . . . . 11 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. ( A X. _V ) )
147		xpopth 6846	. . . . . . . . . . 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 665	. . . . . . . . . 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 256	. . . . . . . . 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 260	. . . . . . . 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 435	. . . . . . 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 7620	. . . . . 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 221	. . . 4 |- ( ph -> ( A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C -> T ~<_ ( A X. C ) ) )
155	154	adantld 468	. . 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 1772	. 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 187   /\ wa 370   = wceq 1437   E.wex 1657   e. wcel 1872   =/= wne 2614   A.wral 2771   E.wrex 2772   _Vcvv 3080   [_csb 3395   C_ wss 3436   (/)c0 3761   {csn 3998   <.cop 4004   U_ciun 4299   class class class wbr 4423   X. cxp 4851   -->wf 5597   -1-1->wf1 5598   ` cfv 5601  (class class class)co 6305   1stc1st 6805   2ndc2nd 6806   ^m cmap 7483   ~<_ cdom 7578  AC wacn 8380

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

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-map 7485  df-dom 7582  df-acn 8384

This theorem is referenced by:  iundomg  8973  iundom  8974