Theorem iundom2g 8375

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 7082	. . . . . . . . 9 |- ( B ~<_ C -> E. g g : B -1-1-> C )
4	3	adantl 453	. . . . . . . 8 |- ( ( x e. A /\ B ~<_ C ) -> E. g g : B -1-1-> C )
5		f1f 5602	. . . . . . . . . . . 12 |- ( g : B -1-1-> C -> g : B --> C )
6		reldom 7078	. . . . . . . . . . . . . . 15 |- Rel ~<_
7	6	brrelex2i 4882	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> C e. _V )
8	6	brrelexi 4881	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> B e. _V )
9		elmapg 6994	. . . . . . . . . . . . . 14 |- ( ( C e. _V /\ B e. _V ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
10	7, 8, 9	syl2anc 643	. . . . . . . . . . . . 13 |- ( B ~<_ C -> ( g e. ( C ^m B ) <-> g : B --> C ) )
11	10	adantl 453	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
12	5, 11	syl5ibr 213	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. ( C ^m B ) ) )
13		ssiun2 4098	. . . . . . . . . . . . 13 |- ( x e. A -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
14	13	adantr 452	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
15	14	sseld 3311	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) -> g e. U_ x e. A ( C ^m B ) ) )
16	12, 15	syld 42	. . . . . . . . . 10 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. U_ x e. A ( C ^m B ) ) )
17	16	ancrd 538	. . . . . . . . 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 ) ) )
18	17	eximdv 1629	. . . . . . . 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 ) ) )
19	4, 18	mpd 15	. . . . . . 7 |- ( ( x e. A /\ B ~<_ C ) -> E. g ( g e. U_ x e. A ( C ^m B ) /\ g : B -1-1-> C ) )
20		df-rex 2676	. . . . . . 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 ) )
21	19, 20	sylibr 204	. . . . . 6 |- ( ( x e. A /\ B ~<_ C ) -> E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
22	21	ralimiaa 2744	. . . . 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 )
23	2, 22	syl 16	. . . 4 |- ( ph -> A. x e. A E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
24		nfv 1626	. . . . 5 |- F/ y E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C
25		nfiu1 4085	. . . . . 6 |- F/_ x U_ x e. A ( C ^m B )
26		nfcv 2544	. . . . . . 7 |- F/_ x g
27		nfcsb1v 3247	. . . . . . 7 |- F/_ x [_ y / x ]_ B
28		nfcv 2544	. . . . . . 7 |- F/_ x C
29	26, 27, 28	nff1 5600	. . . . . 6 |- F/ x g : [_ y / x ]_ B -1-1-> C
30	25, 29	nfrex 2725	. . . . 5 |- F/ x E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C
31		csbeq1a 3223	. . . . . . 7 |- ( x = y -> B = [_ y / x ]_ B )
32		f1eq2 5598	. . . . . . 7 |- ( B = [_ y / x ]_ B -> ( g : B -1-1-> C <-> g : [_ y / x ]_ B -1-1-> C ) )
33	31, 32	syl 16	. . . . . 6 |- ( x = y -> ( g : B -1-1-> C <-> g : [_ y / x ]_ B -1-1-> C ) )
34	33	rexbidv 2691	. . . . 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 ) )
35	24, 30, 34	cbvral 2892	. . . 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 )
36	23, 35	sylib 189	. . 3 |- ( ph -> A. y e. A E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C )
37		f1eq1 5597	. . . 4 |- ( g = ( f ` y ) -> ( g : [_ y / x ]_ B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
38	37	acni3 7888	. . 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 ) )
39	1, 36, 38	syl2anc 643	. 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 ) )
40		nfv 1626	. . . . . 6 |- F/ y ( f ` x ) : B -1-1-> C
41		nfcv 2544	. . . . . . 7 |- F/_ x ( f ` y )
42	41, 27, 28	nff1 5600	. . . . . 6 |- F/ x ( f ` y ) : [_ y / x ]_ B -1-1-> C
43		fveq2 5691	. . . . . . . 8 |- ( x = y -> ( f ` x ) = ( f ` y ) )
44		f1eq1 5597	. . . . . . . 8 |- ( ( f ` x ) = ( f ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : B -1-1-> C ) )
45	43, 44	syl 16	. . . . . . 7 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : B -1-1-> C ) )
46		f1eq2 5598	. . . . . . . 8 |- ( B = [_ y / x ]_ B -> ( ( f ` y ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
47	31, 46	syl 16	. . . . . . 7 |- ( x = y -> ( ( f ` y ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
48	45, 47	bitrd 245	. . . . . 6 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
49	40, 42, 48	cbvral 2892	. . . . 5 |- ( A. x e. A ( f ` x ) : B -1-1-> C <-> A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C )
50		df-ne 2573	. . . . . . . 8 |- ( A =/= (/) <-> -. A = (/) )
51		acnrcl 7883	. . . . . . . . . 10 |- ( U_ x e. A ( C ^m B ) e. AC A -> A e. _V )
52	1, 51	syl 16	. . . . . . . . 9 |- ( ph -> A e. _V )
53		r19.2z 3681	. . . . . . . . . . . 12 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> E. x e. A B ~<_ C )
54	7	rexlimivw 2790	. . . . . . . . . . . 12 |- ( E. x e. A B ~<_ C -> C e. _V )
55	53, 54	syl 16	. . . . . . . . . . 11 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> C e. _V )
56	55	expcom 425	. . . . . . . . . 10 |- ( A. x e. A B ~<_ C -> ( A =/= (/) -> C e. _V ) )
57	2, 56	syl 16	. . . . . . . . 9 |- ( ph -> ( A =/= (/) -> C e. _V ) )
58		xpexg 4952	. . . . . . . . 9 |- ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
59	52, 57, 58	ee12an 1369	. . . . . . . 8 |- ( ph -> ( A =/= (/) -> ( A X. C ) e. _V ) )
60	50, 59	syl5bir 210	. . . . . . 7 |- ( ph -> ( -. A = (/) -> ( A X. C ) e. _V ) )
61		xpeq1 4855	. . . . . . . 8 |- ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
62		xp0r 4919	. . . . . . . . 9 |- ( (/) X. C ) = (/)
63		0ex 4303	. . . . . . . . 9 |- (/) e. _V
64	62, 63	eqeltri 2478	. . . . . . . 8 |- ( (/) X. C ) e. _V
65	61, 64	syl6eqel 2496	. . . . . . 7 |- ( A = (/) -> ( A X. C ) e. _V )
66	60, 65	pm2.61d2 154	. . . . . 6 |- ( ph -> ( A X. C ) e. _V )
67		iunfo.1	. . . . . . . . . 10 |- T = U_ x e. A ( { x } X. B )
68	67	eleq2i 2472	. . . . . . . . 9 |- ( y e. T <-> y e. U_ x e. A ( { x } X. B ) )
69		eliun 4061	. . . . . . . . 9 |- ( y e. U_ x e. A ( { x } X. B ) <-> E. x e. A y e. ( { x } X. B ) )
70	68, 69	bitri 241	. . . . . . . 8 |- ( y e. T <-> E. x e. A y e. ( { x } X. B ) )
71		r19.29 2810	. . . . . . . . . 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 ) ) )
72		xp1st 6339	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 1st ` y ) e. { x } )
73	72	ad2antll 710	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. { x } )
74		elsni 3802	. . . . . . . . . . . . . 14 |- ( ( 1st ` y ) e. { x } -> ( 1st ` y ) = x )
75	73, 74	syl 16	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) = x )
76		simpl 444	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x e. A )
77	75, 76	eqeltrd 2482	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. A )
78	75	fveq2d 5695	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` ( 1st ` y ) ) = ( f ` x ) )
79	78	fveq1d 5693	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) = ( ( f ` x ) ` ( 2nd ` y ) ) )
80		f1f 5602	. . . . . . . . . . . . . . 15 |- ( ( f ` x ) : B -1-1-> C -> ( f ` x ) : B --> C )
81	80	ad2antrl 709	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` x ) : B --> C )
82		xp2nd 6340	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 2nd ` y ) e. B )
83	82	ad2antll 710	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. B )
84	81, 83	ffvelrnd 5834	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` x ) ` ( 2nd ` y ) ) e. C )
85	79, 84	eqeltrd 2482	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C )
86		opelxpi 4873	. . . . . . . . . . . 12 |- ( ( ( 1st ` y ) e. A /\ ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C ) -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) )
87	77, 85, 86	syl2anc 643	. . . . . . . . . . 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 ) )
88	87	rexlimiva 2789	. . . . . . . . . 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 ) )
89	71, 88	syl 16	. . . . . . . . 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 ) )
90	89	ex 424	. . . . . . . 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 ) ) )
91	70, 90	syl5bi 209	. . . . . . 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 ) ) )
92		fvex 5705	. . . . . . . . . 10 |- ( 1st ` y ) e. _V
93		fvex 5705	. . . . . . . . . 10 |- ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. _V
94	92, 93	opth 4399	. . . . . . . . 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 ) ) ) )
95		simpr 448	. . . . . . . . . . . . . . 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 ) )
96	95	fveq2d 5695	. . . . . . . . . . . . . 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 ) ) )
97	96	fveq1d 5693	. . . . . . . . . . . . 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 ) ) )
98	97	eqeq2d 2419	. . . . . . . . . . . 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 ) ) ) )
99		djussxp 4981	. . . . . . . . . . . . . . . . . 18 |- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
100	67, 99	eqsstri 3342	. . . . . . . . . . . . . . . . 17 |- T C_ ( A X. _V )
101		simprl 733	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. T )
102	100, 101	sseldi 3310	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. ( A X. _V ) )
103	102	adantr 452	. . . . . . . . . . . . . . 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 ) )
104		xp1st 6339	. . . . . . . . . . . . . . 15 |- ( y e. ( A X. _V ) -> ( 1st ` y ) e. A )
105	103, 104	syl 16	. . . . . . . . . . . . . 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 )
106		simpll 731	. . . . . . . . . . . . . 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 )
107		nfcv 2544	. . . . . . . . . . . . . . . 16 |- F/_ x ( f ` ( 1st ` y ) )
108		nfcsb1v 3247	. . . . . . . . . . . . . . . 16 |- F/_ x [_ ( 1st ` y ) / x ]_ B
109	107, 108, 28	nff1 5600	. . . . . . . . . . . . . . 15 |- F/ x ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C
110		fveq2 5691	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> ( f ` x ) = ( f ` ( 1st ` y ) ) )
111		f1eq1 5597	. . . . . . . . . . . . . . . . 17 |- ( ( f ` x ) = ( f ` ( 1st ` y ) ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : B -1-1-> C ) )
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : B -1-1-> C ) )
113		csbeq1a 3223	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> B = [_ ( 1st ` y ) / x ]_ B )
114		f1eq2 5598	. . . . . . . . . . . . . . . . 17 |- ( B = [_ ( 1st ` y ) / x ]_ B -> ( ( f ` ( 1st ` y ) ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
115	113, 114	syl 16	. . . . . . . . . . . . . . . 16 |- ( x = ( 1st ` y ) -> ( ( f ` ( 1st ` y ) ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
116	112, 115	bitrd 245	. . . . . . . . . . . . . . 15 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
117	109, 116	rspc 3010	. . . . . . . . . . . . . 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 ) )
118	105, 106, 117	sylc 58	. . . . . . . . . . . . 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 )
119	108	nfel2 2556	. . . . . . . . . . . . . . . . . . . 20 |- F/ x ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B
120	75	eqcomd 2413	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x = ( 1st ` y ) )
121	120, 113	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> B = [_ ( 1st ` y ) / x ]_ B )
122	83, 121	eleqtrd 2484	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
123	122	ex 424	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. A -> ( ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
124	119, 123	rexlimi 2787	. . . . . . . . . . . . . . . . . . 19 |- ( E. x e. A ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
125	71, 124	syl 16	. . . . . . . . . . . . . . . . . 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 )
126	125	ex 424	. . . . . . . . . . . . . . . . 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 ) )
127	70, 126	syl5bi 209	. . . . . . . . . . . . . . . 16 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
128	127	imp 419	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ y e. T ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
129	128	adantrr 698	. . . . . . . . . . . . . 14 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
130	129	adantr 452	. . . . . . . . . . . . 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 )
131	127	ralrimiv 2752	. . . . . . . . . . . . . . . . 17 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
132		fveq2 5691	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( 2nd ` y ) = ( 2nd ` z ) )
133		fveq2 5691	. . . . . . . . . . . . . . . . . . . 20 |- ( y = z -> ( 1st ` y ) = ( 1st ` z ) )
134	133	csbeq1d 3221	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
135	132, 134	eleq12d 2476	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B <-> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B ) )
136	135	rspccva 3015	. . . . . . . . . . . . . . . . 17 |- ( ( A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
137	131, 136	sylan 458	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
138	137	adantrl 697	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
139	138	adantr 452	. . . . . . . . . . . . . 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 )
140	95	csbeq1d 3221	. . . . . . . . . . . . . 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 )
141	139, 140	eleqtrrd 2485	. . . . . . . . . . . . 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 )
142		f1fveq 5971	. . . . . . . . . . . . 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 ) ) )
143	118, 130, 141, 142	syl12anc 1182	. . . . . . . . . . . 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 ) ) )
144	98, 143	bitr3d 247	. . . . . . . . . . 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 ) ) )
145	144	pm5.32da 623	. . . . . . . . . 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 ) ) ) )
146		simprr 734	. . . . . . . . . . . 12 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. T )
147	100, 146	sseldi 3310	. . . . . . . . . . 11 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. ( A X. _V ) )
148		xpopth 6351	. . . . . . . . . . 11 |- ( ( y e. ( A X. _V ) /\ z e. ( A X. _V ) ) -> ( ( ( 1st ` y ) = ( 1st ` z ) /\ ( 2nd ` y ) = ( 2nd ` z ) ) <-> y = z ) )
149	102, 147, 148	syl2anc 643	. . . . . . . . . 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 ) )
150	145, 149	bitrd 245	. . . . . . . . 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 ) )
151	94, 150	syl5bb 249	. . . . . . . 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 ) )
152	151	ex 424	. . . . . . 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 ) ) )
153	91, 152	dom2d 7111	. . . . . 6 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( ( A X. C ) e. _V -> T ~<_ ( A X. C ) ) )
154	66, 153	syl5com 28	. . . . 5 |- ( ph -> ( A. x e. A ( f ` x ) : B -1-1-> C -> T ~<_ ( A X. C ) ) )
155	49, 154	syl5bir 210	. . . 4 |- ( ph -> ( A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C -> T ~<_ ( A X. C ) ) )
156	155	adantld 454	. . 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 ) ) )
157	156	exlimdv 1643	. 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 ) ) )
158	39, 157	mpd 15	1 |- ( ph -> T ~<_ ( A X. C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2571   A.wral 2670   E.wrex 2671   _Vcvv 2920   [_csb 3215   C_ wss 3284   (/)c0 3592   {csn 3778   <.cop 3781   U_ciun 4057   class class class wbr 4176   X. cxp 4839   -->wf 5413   -1-1->wf1 5414   ` cfv 5417  (class class class)co 6044   1stc1st 6310   2ndc2nd 6311   ^m cmap 6981   ~<_ cdom 7070  AC wacn 7785

This theorem is referenced by:  iundomg  8376  iundom  8377

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-1st 6312  df-2nd 6313  df-map 6983  df-dom 7074  df-acn 7789