Theorem iundom2g 8918

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 7529	. . . . . . . . 9 |- ( B ~<_ C -> E. g g : B -1-1-> C )
4	3	adantl 466	. . . . . . . 8 |- ( ( x e. A /\ B ~<_ C ) -> E. g g : B -1-1-> C )
5		f1f 5771	. . . . . . . . . . . 12 |- ( g : B -1-1-> C -> g : B --> C )
6		reldom 7524	. . . . . . . . . . . . . . 15 |- Rel ~<_
7	6	brrelex2i 5031	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> C e. _V )
8	6	brrelexi 5030	. . . . . . . . . . . . . 14 |- ( B ~<_ C -> B e. _V )
9		elmapg 7435	. . . . . . . . . . . . . 14 |- ( ( C e. _V /\ B e. _V ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
10	7, 8, 9	syl2anc 661	. . . . . . . . . . . . 13 |- ( B ~<_ C -> ( g e. ( C ^m B ) <-> g : B --> C ) )
11	10	adantl 466	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
12	5, 11	syl5ibr 221	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. ( C ^m B ) ) )
13		ssiun2 4358	. . . . . . . . . . . . 13 |- ( x e. A -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
14	13	adantr 465	. . . . . . . . . . . 12 |- ( ( x e. A /\ B ~<_ C ) -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
15	14	sseld 3488	. . . . . . . . . . 11 |- ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) -> g e. U_ x e. A ( C ^m B ) ) )
16	12, 15	syld 44	. . . . . . . . . 10 |- ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. U_ x e. A ( C ^m B ) ) )
17	16	ancrd 554	. . . . . . . . 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 1697	. . . . . . . 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 2799	. . . . . . 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 212	. . . . . 6 |- ( ( x e. A /\ B ~<_ C ) -> E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
22	21	ralimiaa 2835	. . . . 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 1694	. . . . 5 |- F/ y E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C
25		nfiu1 4345	. . . . . 6 |- F/_ x U_ x e. A ( C ^m B )
26		nfcv 2605	. . . . . . 7 |- F/_ x g
27		nfcsb1v 3436	. . . . . . 7 |- F/_ x [_ y / x ]_ B
28		nfcv 2605	. . . . . . 7 |- F/_ x C
29	26, 27, 28	nff1 5769	. . . . . 6 |- F/ x g : [_ y / x ]_ B -1-1-> C
30	25, 29	nfrex 2906	. . . . 5 |- F/ x E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C
31		csbeq1a 3429	. . . . . . 7 |- ( x = y -> B = [_ y / x ]_ B )
32		f1eq2 5767	. . . . . . 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 2954	. . . . 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 3066	. . . 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 196	. . 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 5766	. . . 4 |- ( g = ( f ` y ) -> ( g : [_ y / x ]_ B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
38	37	acni3 8431	. . 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 661	. 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 1694	. . . . . 6 |- F/ y ( f ` x ) : B -1-1-> C
41		nfcv 2605	. . . . . . 7 |- F/_ x ( f ` y )
42	41, 27, 28	nff1 5769	. . . . . 6 |- F/ x ( f ` y ) : [_ y / x ]_ B -1-1-> C
43		fveq2 5856	. . . . . . . 8 |- ( x = y -> ( f ` x ) = ( f ` y ) )
44		f1eq1 5766	. . . . . . . 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 5767	. . . . . . . 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 253	. . . . . 6 |- ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
49	40, 42, 48	cbvral 3066	. . . . 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 2640	. . . . . . . 8 |- ( A =/= (/) <-> -. A = (/) )
51		acnrcl 8426	. . . . . . . . . 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 3904	. . . . . . . . . . . 12 |- ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> E. x e. A B ~<_ C )
54	7	rexlimivw 2932	. . . . . . . . . . . 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 435	. . . . . . . . . 10 |- ( A. x e. A B ~<_ C -> ( A =/= (/) -> C e. _V ) )
57	2, 56	syl 16	. . . . . . . . 9 |- ( ph -> ( A =/= (/) -> C e. _V ) )
58		xpexg 6587	. . . . . . . . 9 |- ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
59	52, 57, 58	syl6an 545	. . . . . . . 8 |- ( ph -> ( A =/= (/) -> ( A X. C ) e. _V ) )
60	50, 59	syl5bir 218	. . . . . . 7 |- ( ph -> ( -. A = (/) -> ( A X. C ) e. _V ) )
61		xpeq1 5003	. . . . . . . 8 |- ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
62		0xp 5070	. . . . . . . . 9 |- ( (/) X. C ) = (/)
63		0ex 4567	. . . . . . . . 9 |- (/) e. _V
64	62, 63	eqeltri 2527	. . . . . . . 8 |- ( (/) X. C ) e. _V
65	61, 64	syl6eqel 2539	. . . . . . 7 |- ( A = (/) -> ( A X. C ) e. _V )
66	60, 65	pm2.61d2 160	. . . . . 6 |- ( ph -> ( A X. C ) e. _V )
67		iunfo.1	. . . . . . . . . 10 |- T = U_ x e. A ( { x } X. B )
68	67	eleq2i 2521	. . . . . . . . 9 |- ( y e. T <-> y e. U_ x e. A ( { x } X. B ) )
69		eliun 4320	. . . . . . . . 9 |- ( y e. U_ x e. A ( { x } X. B ) <-> E. x e. A y e. ( { x } X. B ) )
70	68, 69	bitri 249	. . . . . . . 8 |- ( y e. T <-> E. x e. A y e. ( { x } X. B ) )
71		r19.29 2978	. . . . . . . . . 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 6815	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 1st ` y ) e. { x } )
73	72	ad2antll 728	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. { x } )
74		elsni 4039	. . . . . . . . . . . . . 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 457	. . . . . . . . . . . . 13 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x e. A )
77	75, 76	eqeltrd 2531	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. A )
78	75	fveq2d 5860	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` ( 1st ` y ) ) = ( f ` x ) )
79	78	fveq1d 5858	. . . . . . . . . . . . 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 5771	. . . . . . . . . . . . . . 15 |- ( ( f ` x ) : B -1-1-> C -> ( f ` x ) : B --> C )
81	80	ad2antrl 727	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` x ) : B --> C )
82		xp2nd 6816	. . . . . . . . . . . . . . 15 |- ( y e. ( { x } X. B ) -> ( 2nd ` y ) e. B )
83	82	ad2antll 728	. . . . . . . . . . . . . 14 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. B )
84	81, 83	ffvelrnd 6017	. . . . . . . . . . . . 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 2531	. . . . . . . . . . . 12 |- ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C )
86		opelxpi 5021	. . . . . . . . . . . 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 661	. . . . . . . . . . 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 2931	. . . . . . . . . 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 434	. . . . . . . 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 217	. . . . . . 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 5866	. . . . . . . . . 10 |- ( 1st ` y ) e. _V
93		fvex 5866	. . . . . . . . . 10 |- ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. _V
94	92, 93	opth 4711	. . . . . . . . 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 461	. . . . . . . . . . . . . . 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 5860	. . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . 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 2457	. . . . . . . . . . . 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 5138	. . . . . . . . . . . . . . . . . 18 |- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
100	67, 99	eqsstri 3519	. . . . . . . . . . . . . . . . 17 |- T C_ ( A X. _V )
101		simprl 756	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. T )
102	100, 101	sseldi 3487	. . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 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 6815	. . . . . . . . . . . . . . 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 753	. . . . . . . . . . . . . 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 2605	. . . . . . . . . . . . . . . 16 |- F/_ x ( f ` ( 1st ` y ) )
108		nfcsb1v 3436	. . . . . . . . . . . . . . . 16 |- F/_ x [_ ( 1st ` y ) / x ]_ B
109	107, 108, 28	nff1 5769	. . . . . . . . . . . . . . 15 |- F/ x ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C
110		fveq2 5856	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> ( f ` x ) = ( f ` ( 1st ` y ) ) )
111		f1eq1 5766	. . . . . . . . . . . . . . . . 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 3429	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` y ) -> B = [_ ( 1st ` y ) / x ]_ B )
114		f1eq2 5767	. . . . . . . . . . . . . . . . 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 253	. . . . . . . . . . . . . . 15 |- ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
117	109, 116	rspc 3190	. . . . . . . . . . . . . 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 60	. . . . . . . . . . . . 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 2623	. . . . . . . . . . . . . . . . . . . 20 |- F/ x ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B
120	75	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . . . 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 2533	. . . . . . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . . . . . 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 2925	. . . . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . 16 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
128	127	imp 429	. . . . . . . . . . . . . . 15 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ y e. T ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
129	128	adantrr 716	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . . 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 2855	. . . . . . . . . . . . . . . . 17 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
132		fveq2 5856	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( 2nd ` y ) = ( 2nd ` z ) )
133		fveq2 5856	. . . . . . . . . . . . . . . . . . . 20 |- ( y = z -> ( 1st ` y ) = ( 1st ` z ) )
134	133	csbeq1d 3427	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
135	132, 134	eleq12d 2525	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B <-> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B ) )
136	135	rspccva 3195	. . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
138	137	adantrl 715	. . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . 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 3427	. . . . . . . . . . . . . 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 2534	. . . . . . . . . . . . 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 6155	. . . . . . . . . . . . 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 1227	. . . . . . . . . . . 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 255	. . . . . . . . . . 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 641	. . . . . . . . . 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 757	. . . . . . . . . . . 12 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. T )
147	100, 146	sseldi 3487	. . . . . . . . . . 11 |- ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. ( A X. _V ) )
148		xpopth 6824	. . . . . . . . . . 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 661	. . . . . . . . . 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 253	. . . . . . . . 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 257	. . . . . . . 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 434	. . . . . . 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 7558	. . . . . 6 |- ( A. x e. A ( f ` x ) : B -1-1-> C -> ( ( A X. C ) e. _V -> T ~<_ ( A X. C ) ) )
154	66, 153	syl5com 30	. . . . 5 |- ( ph -> ( A. x e. A ( f ` x ) : B -1-1-> C -> T ~<_ ( A X. C ) ) )
155	49, 154	syl5bir 218	. . . 4 |- ( ph -> ( A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C -> T ~<_ ( A X. C ) ) )
156	155	adantld 467	. . 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 1711	. 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 184   /\ wa 369   = wceq 1383   E.wex 1599   e. wcel 1804   =/= wne 2638   A.wral 2793   E.wrex 2794   _Vcvv 3095   [_csb 3420   C_ wss 3461   (/)c0 3770   {csn 4014   <.cop 4020   U_ciun 4315   class class class wbr 4437   X. cxp 4987   -->wf 5574   -1-1->wf1 5575   ` cfv 5578  (class class class)co 6281   1stc1st 6783   2ndc2nd 6784   ^m cmap 7422   ~<_ cdom 7516  AC wacn 8322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-1st 6785  df-2nd 6786  df-map 7424  df-dom 7520  df-acn 8326

This theorem is referenced by:  iundomg  8919  iundom  8920