Theorem iundom2g 8983

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 7598	. . . . . . . . 9 |- ( B ~<_ C -> E. g g : B -1-1-> C )
4	3	adantl 473	. . . . . . . 8 |- ( ( x e. A /\ B ~<_ C ) -> E. g g : B -1-1-> C )
5		f1f 5792	. . . . . . . . . . . 12 |- ( g : B -1-1-> C -> g : B --> C )
6		reldom 7593	. . . . . . . . . . . . . . 15 |- Rel ~<_
7	6	brrelex2i 4881	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> C e. _V )
8	6	brrelexi 4880	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> B e. _V )
9	7, 8	elmapd 7504	. . . . . . . . . . . . 13 |- ( B ~<_ C -> ( g e. ( C ^m B ) <-> g : B --> C ) )
10	9	adantl 473	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
11	5, 10	syl5ibr 229	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. ( C ^m B ) ) )
12		ssiun2 4312	. . . . . . . . . . . . 13 |- ( x e. A -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
13	12	adantr 472	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
14	13	sseld 3417	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) -> g e. U_ x e. A ( C ^m B ) ) )
15	11, 14	syld 44	. . . . . . . . . 10 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. U_ x e. A ( C ^m B ) ) )
16	15	ancrd 563	. . . . . . . . 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 1772	. . . . . . . 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 2762	. . . . . . 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 217	. . . . . 6 |- ( ( x e. A /\ B ~<_ C ) -> E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
21	20	ralimiaa 2795	. . . . 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 1769	. . . . 5 |- F/ y E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C
24		nfiu1 4299	. . . . . 6 |- F/_ x U_ x e. A ( C ^m B )
25		nfcv 2612	. . . . . . 7 |- F/_ x g
26		nfcsb1v 3365	. . . . . . 7 |- F/_ x [_ y / x ]_ B
27		nfcv 2612	. . . . . . 7 |- F/_ x C
28	25, 26, 27	nff1 5790	. . . . . 6 |- F/ x g : [_ y / x ]_ B -1-1-> C
29	24, 28	nfrex 2848	. . . . 5 |- F/ x E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C
30		csbeq1a 3358	. . . . . . 7 |- ( x = y -> B = [_ y / x ]_ B )
31		f1eq2 5788	. . . . . . 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 2892	. . . . 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 3001	. . . 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 201	. . 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 5787	. . . 4 |- ( g = ( f ` y ) -> ( g : [_ y / x ]_ B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
37	36	acni3 8496	. . 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 673	. 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 1769	. . . . . 6 |- F/ y ( f ` x ) : B -1-1-> C
40		nfcv 2612	. . . . . . 7 |- F/_ x ( f ` y )
41	40, 26, 27	nff1 5790	. . . . . 6 |- F/ x ( f ` y ) : [_ y / x ]_ B -1-1-> C
42		fveq2 5879	. . . . . . . 8 |- ( x = y -> ( f ` x ) = ( f ` y ) )
43		f1eq1 5787	. . . . . . . 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 5788	. . . . . . . 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 261	. . . . . 6 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
48	39, 41, 47	cbvral 3001	. . . . 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 2643	. . . . . . . 8 |- ( A =/= (/) <-> -. A = (/) )
50		acnrcl 8491	. . . . . . . . . 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 3849	. . . . . . . . . . . 12 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> E. x e. A B ~<_ C )
53	7	rexlimivw 2869	. . . . . . . . . . . 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 442	. . . . . . . . . 10 |- ( A. x e. A B ~<_ C -> ( A =/= (/) -> C e. _V ) )
56	2, 55	syl 17	. . . . . . . . 9 |- ( ph -> ( A =/= (/) -> C e. _V ) )
57		xpexg 6612	. . . . . . . . 9 |- ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
58	51, 56, 57	syl6an 554	. . . . . . . 8 |- ( ph -> ( A =/= (/) -> ( A X. C ) e. _V ) )
59	49, 58	syl5bir 226	. . . . . . 7 |- ( ph -> ( -. A = (/) -> ( A X. C ) e. _V ) )
60		xpeq1 4853	. . . . . . . 8 |- ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
61		0xp 4920	. . . . . . . . 9 |- ( (/) X. C ) = (/)
62		0ex 4528	. . . . . . . . 9 |- (/) e. _V
63	61, 62	eqeltri 2545	. . . . . . . 8 |- ( (/) X. C ) e. _V
64	60, 63	syl6eqel 2557	. . . . . . 7 |- ( A = (/) -> ( A X. C ) e. _V )
65	59, 64	pm2.61d2 165	. . . . . 6 |- ( ph -> ( A X. C ) e. _V )
66		iunfo.1	. . . . . . . . . 10 |- T = U_ x e. A ( { x } X. B )
67	66	eleq2i 2541	. . . . . . . . 9 |- ( y e. T <-> y e. U_ x e. A ( { x } X. B ) )
68		eliun 4274	. . . . . . . . 9 |- ( y e. U_ x e. A ( { x } X. B ) <-> E. x e. A y e. ( { x } X. B ) )
69	67, 68	bitri 257	. . . . . . . 8 |- ( y e. T <-> E. x e. A y e. ( { x } X. B ) )
70		r19.29 2912	. . . . . . . . . 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 6842	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 1st ` y ) e. { x } )
72	71	ad2antll 743	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. { x } )
73		elsni 3985	. . . . . . . . . . . . . 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 464	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x e. A )
76	74, 75	eqeltrd 2549	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. A )
77	74	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` ( 1st ` y ) ) = ( f ` x ) )
78	77	fveq1d 5881	. . . . . . . . . . . . 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 5792	. . . . . . . . . . . . . . 15 |- ( ( f ` x ) : B -1-1-> C -> ( f ` x ) : B --> C )
80	79	ad2antrl 742	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` x ) : B --> C )
81		xp2nd 6843	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 2nd ` y ) e. B )
82	81	ad2antll 743	. . . . . . . . . . . . . 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 2549	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C )
85		opelxpi 4871	. . . . . . . . . . . 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 673	. . . . . . . . . . 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 2868	. . . . . . . . . 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 441	. . . . . . . 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 225	. . . . . . 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 5889	. . . . . . . . . 10 |- ( 1st ` y ) e. _V
92		fvex 5889	. . . . . . . . . 10 |- ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. _V
93	91, 92	opth 4676	. . . . . . . . 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 468	. . . . . . . . . . . . . . 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 5883	. . . . . . . . . . . . . 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 5881	. . . . . . . . . . . . 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 2481	. . . . . . . . . . . 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 4985	. . . . . . . . . . . . . . . . . 18 |- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
99	66, 98	eqsstri 3448	. . . . . . . . . . . . . . . . 17 |- T C_ ( A X. _V )
100		simprl 772	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. T )
101	99, 100	sseldi 3416	. . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . 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 2612	. . . . . . . . . . . . . . . 16 |- F/_ x ( f ` ( 1st ` y ) )
107		nfcsb1v 3365	. . . . . . . . . . . . . . . 16 |- F/_ x [_ ( 1st ` y ) / x ]_ B
108	106, 107, 27	nff1 5790	. . . . . . . . . . . . . . 15 |- F/ x ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C
109		fveq2 5879	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> ( f ` x ) = ( f ` ( 1st ` y ) ) )
110		f1eq1 5787	. . . . . . . . . . . . . . . . 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 3358	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> B = [_ ( 1st ` y ) / x ]_ B )
113		f1eq2 5788	. . . . . . . . . . . . . . . . 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 261	. . . . . . . . . . . . . . 15 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
116	108, 115	rspc 3130	. . . . . . . . . . . . . 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 61	. . . . . . . . . . . . 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 2628	. . . . . . . . . . . . . . . . . . . 20 |- F/ x ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B
119	74	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . 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 2551	. . . . . . . . . . . . . . . . . . . . 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 441	. . . . . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . . . . . 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 441	. . . . . . . . . . . . . . . . 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 225	. . . . . . . . . . . . . . . 16 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
127	126	imp 436	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ y e. T ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
128	127	adantrr 731	. . . . . . . . . . . . . 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 472	. . . . . . . . . . . . 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 2808	. . . . . . . . . . . . . . . . 17 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
131		fveq2 5879	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( 2nd ` y ) = ( 2nd ` z ) )
132		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( y = z -> ( 1st ` y ) = ( 1st ` z ) )
133	132	csbeq1d 3356	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
134	131, 133	eleq12d 2543	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B <-> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B ) )
135	134	rspccva 3135	. . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
137	136	adantrl 730	. . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . 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 3356	. . . . . . . . . . . . . 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 2552	. . . . . . . . . . . . 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 6181	. . . . . . . . . . . . 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 1290	. . . . . . . . . . . 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 263	. . . . . . . . . . 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 653	. . . . . . . . . 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 774	. . . . . . . . . . . 12 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. T )
146	99, 145	sseldi 3416	. . . . . . . . . . 11 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. ( A X. _V ) )
147		xpopth 6851	. . . . . . . . . . 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 673	. . . . . . . . . 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 261	. . . . . . . . 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 265	. . . . . . . 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 441	. . . . . . 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 7628	. . . . . 6 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( ( A X. C ) e. _V -> T ~<_ ( A X. C ) ) )
153	65, 152	syl5com 30	. . . . 5 |- ( ph -> ( A. x e. A ( f ` x ) : B -1-1-> C -> T ~<_ ( A X. C ) ) )
154	48, 153	syl5bir 226	. . . 4 |- ( ph -> ( A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C -> T ~<_ ( A X. C ) ) )
155	154	adantld 474	. . 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 1787	. 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 189   /\ wa 376   = wceq 1452   E.wex 1671   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031   [_csb 3349   C_ wss 3390   (/)c0 3722   {csn 3959   <.cop 3965   U_ciun 4269   class class class wbr 4395   X. cxp 4837   -->wf 5585   -1-1->wf1 5586   ` cfv 5589  (class class class)co 6308   1stc1st 6810   2ndc2nd 6811   ^m cmap 7490   ~<_ cdom 7585  AC wacn 8390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-map 7492  df-dom 7589  df-acn 8394

This theorem is referenced by:  iundomg  8984  iundom  8985