Metamath Proof Explorer

Theorem iundom2g

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)

Ref Expression
Hypotheses 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 iundom2g 
|- ( ph -> T ~<_ ( A X. C ) )

Proof

Step Hyp Ref Expression
1 iunfo.1 
 |-  T = U_ x e. A ( { x } X. B )
2 iundomg.2 
 |-  ( ph -> U_ x e. A ( C ^m B ) e. AC_ A )
3 iundomg.3 
 |-  ( ph -> A. x e. A B ~<_ C )
4 brdomi 
 |-  ( B ~<_ C -> E. g g : B -1-1-> C )
5 4 adantl 
 |-  ( ( x e. A /\ B ~<_ C ) -> E. g g : B -1-1-> C )
6 f1f 
 |-  ( g : B -1-1-> C -> g : B --> C )
7 reldom 
 |-  Rel ~<_
8 7 brrelex2i 
 |-  ( B ~<_ C -> C e. _V )
9 7 brrelex1i 
 |-  ( B ~<_ C -> B e. _V )
10 8 9 elmapd 
 |-  ( B ~<_ C -> ( g e. ( C ^m B ) <-> g : B --> C ) )
11 10 adantl 
 |-  ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) <-> g : B --> C ) )
12 6 11 imbitrrid 
 |-  ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. ( C ^m B ) ) )
13 ssiun2 
 |-  ( x e. A -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
14 13 adantr 
 |-  ( ( x e. A /\ B ~<_ C ) -> ( C ^m B ) C_ U_ x e. A ( C ^m B ) )
15 14 sseld 
 |-  ( ( x e. A /\ B ~<_ C ) -> ( g e. ( C ^m B ) -> g e. U_ x e. A ( C ^m B ) ) )
16 12 15 syld 
 |-  ( ( x e. A /\ B ~<_ C ) -> ( g : B -1-1-> C -> g e. U_ x e. A ( C ^m B ) ) )
17 16 ancrd 
 |-  ( ( 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 
 |-  ( ( 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 5 18 mpd 
 |-  ( ( x e. A /\ B ~<_ C ) -> E. g ( g e. U_ x e. A ( C ^m B ) /\ g : B -1-1-> C ) )
20 df-rex 
 |-  ( 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 
 |-  ( ( x e. A /\ B ~<_ C ) -> E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
22 21 ralimiaa 
 |-  ( 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 3 22 syl 
 |-  ( ph -> A. x e. A E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C )
24 nfv 
 |-  F/ y E. g e. U_ x e. A ( C ^m B ) g : B -1-1-> C
25 nfiu1 
 |-  F/_ x U_ x e. A ( C ^m B )
26 nfcv 
 |-  F/_ x g
27 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
28 nfcv 
 |-  F/_ x C
29 26 27 28 nff1 
 |-  F/ x g : [_ y / x ]_ B -1-1-> C
30 25 29 nfrexw 
 |-  F/ x E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C
31 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
32 f1eq2 
 |-  ( B = [_ y / x ]_ B -> ( g : B -1-1-> C <-> g : [_ y / x ]_ B -1-1-> C ) )
33 31 32 syl 
 |-  ( x = y -> ( g : B -1-1-> C <-> g : [_ y / x ]_ B -1-1-> C ) )
34 33 rexbidv 
 |-  ( 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 cbvralw 
 |-  ( 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 
 |-  ( ph -> A. y e. A E. g e. U_ x e. A ( C ^m B ) g : [_ y / x ]_ B -1-1-> C )
37 f1eq1 
 |-  ( g = ( f ` y ) -> ( g : [_ y / x ]_ B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
38 37 acni3 
 |-  ( ( 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 2 36 38 syl2anc 
 |-  ( 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 
 |-  F/ y ( f ` x ) : B -1-1-> C
41 nfcv 
 |-  F/_ x ( f ` y )
42 41 27 28 nff1 
 |-  F/ x ( f ` y ) : [_ y / x ]_ B -1-1-> C
43 fveq2 
 |-  ( x = y -> ( f ` x ) = ( f ` y ) )
44 f1eq1 
 |-  ( ( f ` x ) = ( f ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : B -1-1-> C ) )
45 43 44 syl 
 |-  ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : B -1-1-> C ) )
46 f1eq2 
 |-  ( B = [_ y / x ]_ B -> ( ( f ` y ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
47 31 46 syl 
 |-  ( x = y -> ( ( f ` y ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
48 45 47 bitrd 
 |-  ( x = y -> ( ( f ` x ) : B -1-1-> C <-> ( f ` y ) : [_ y / x ]_ B -1-1-> C ) )
49 40 42 48 cbvralw 
 |-  ( 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 
 |-  ( A =/= (/) <-> -. A = (/) )
51 acnrcl 
 |-  ( U_ x e. A ( C ^m B ) e. AC_ A -> A e. _V )
52 2 51 syl 
 |-  ( ph -> A e. _V )
53 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> E. x e. A B ~<_ C )
54 8 rexlimivw 
 |-  ( E. x e. A B ~<_ C -> C e. _V )
55 53 54 syl 
 |-  ( ( A =/= (/) /\ A. x e. A B ~<_ C ) -> C e. _V )
56 55 expcom 
 |-  ( A. x e. A B ~<_ C -> ( A =/= (/) -> C e. _V ) )
57 3 56 syl 
 |-  ( ph -> ( A =/= (/) -> C e. _V ) )
58 xpexg 
 |-  ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
59 52 57 58 syl6an 
 |-  ( ph -> ( A =/= (/) -> ( A X. C ) e. _V ) )
60 50 59 biimtrrid 
 |-  ( ph -> ( -. A = (/) -> ( A X. C ) e. _V ) )
61 xpeq1 
 |-  ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
62 0xp 
 |-  ( (/) X. C ) = (/)
63 0ex 
 |-  (/) e. _V
64 62 63 eqeltri 
 |-  ( (/) X. C ) e. _V
65 61 64 eqeltrdi 
 |-  ( A = (/) -> ( A X. C ) e. _V )
66 60 65 pm2.61d2 
 |-  ( ph -> ( A X. C ) e. _V )
67 1 eleq2i 
 |-  ( y e. T <-> y e. U_ x e. A ( { x } X. B ) )
68 eliun 
 |-  ( y e. U_ x e. A ( { x } X. B ) <-> E. x e. A y e. ( { x } X. B ) )
69 67 68 bitri 
 |-  ( y e. T <-> E. x e. A y e. ( { x } X. B ) )
70 r19.29 
 |-  ( ( 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 
 |-  ( y e. ( { x } X. B ) -> ( 1st ` y ) e. { x } )
72 71 ad2antll 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. { x } )
73 elsni 
 |-  ( ( 1st ` y ) e. { x } -> ( 1st ` y ) = x )
74 72 73 syl 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) = x )
75 simpl 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x e. A )
76 74 75 eqeltrd 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 1st ` y ) e. A )
77 74 fveq2d 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` ( 1st ` y ) ) = ( f ` x ) )
78 77 fveq1d 
 |-  ( ( 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 
 |-  ( ( f ` x ) : B -1-1-> C -> ( f ` x ) : B --> C )
80 79 ad2antrl 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( f ` x ) : B --> C )
81 xp2nd 
 |-  ( y e. ( { x } X. B ) -> ( 2nd ` y ) e. B )
82 81 ad2antll 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. B )
83 80 82 ffvelcdmd 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` x ) ` ( 2nd ` y ) ) e. C )
84 78 83 eqeltrd 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. C )
85 76 84 opelxpd 
 |-  ( ( 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 ) )
86 85 rexlimiva 
 |-  ( 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 ) )
87 70 86 syl 
 |-  ( ( 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 ) )
88 87 ex 
 |-  ( 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 69 88 biimtrid 
 |-  ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> <. ( 1st ` y ) , ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) >. e. ( A X. C ) ) )
90 fvex 
 |-  ( 1st ` y ) e. _V
91 fvex 
 |-  ( ( f ` ( 1st ` y ) ) ` ( 2nd ` y ) ) e. _V
92 90 91 opth 
 |-  ( <. ( 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 ) ) ) )
93 simpr 
 |-  ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 1st ` y ) = ( 1st ` z ) )
94 93 fveq2d 
 |-  ( ( ( 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 ) ) )
95 94 fveq1d 
 |-  ( ( ( 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 ) ) )
96 95 eqeq2d 
 |-  ( ( ( 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 ) ) ) )
97 djussxp 
 |-  U_ x e. A ( { x } X. B ) C_ ( A X. _V )
98 1 97 eqsstri 
 |-  T C_ ( A X. _V )
99 simprl 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. T )
100 98 99 sselid 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> y e. ( A X. _V ) )
101 100 adantr 
 |-  ( ( ( 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 ) )
102 xp1st 
 |-  ( y e. ( A X. _V ) -> ( 1st ` y ) e. A )
103 101 102 syl 
 |-  ( ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) /\ ( 1st ` y ) = ( 1st ` z ) ) -> ( 1st ` y ) e. A )
104 simpll 
 |-  ( ( ( 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 )
105 nfcv 
 |-  F/_ x ( f ` ( 1st ` y ) )
106 nfcsb1v 
 |-  F/_ x [_ ( 1st ` y ) / x ]_ B
107 105 106 28 nff1 
 |-  F/ x ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C
108 fveq2 
 |-  ( x = ( 1st ` y ) -> ( f ` x ) = ( f ` ( 1st ` y ) ) )
109 f1eq1 
 |-  ( ( f ` x ) = ( f ` ( 1st ` y ) ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : B -1-1-> C ) )
110 108 109 syl 
 |-  ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : B -1-1-> C ) )
111 csbeq1a 
 |-  ( x = ( 1st ` y ) -> B = [_ ( 1st ` y ) / x ]_ B )
112 f1eq2 
 |-  ( B = [_ ( 1st ` y ) / x ]_ B -> ( ( f ` ( 1st ` y ) ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
113 111 112 syl 
 |-  ( x = ( 1st ` y ) -> ( ( f ` ( 1st ` y ) ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
114 110 113 bitrd 
 |-  ( x = ( 1st ` y ) -> ( ( f ` x ) : B -1-1-> C <-> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
115 107 114 rspc 
 |-  ( ( 1st ` y ) e. A -> ( A. x e. A ( f ` x ) : B -1-1-> C -> ( f ` ( 1st ` y ) ) : [_ ( 1st ` y ) / x ]_ B -1-1-> C ) )
116 103 104 115 sylc 
 |-  ( ( ( 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 )
117 106 nfel2 
 |-  F/ x ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B
118 74 eqcomd 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> x = ( 1st ` y ) )
119 118 111 syl 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> B = [_ ( 1st ` y ) / x ]_ B )
120 82 119 eleqtrd 
 |-  ( ( x e. A /\ ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
121 120 ex 
 |-  ( x e. A -> ( ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
122 117 121 rexlimi 
 |-  ( E. x e. A ( ( f ` x ) : B -1-1-> C /\ y e. ( { x } X. B ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
123 70 122 syl 
 |-  ( ( 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 )
124 123 ex 
 |-  ( 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 69 124 biimtrid 
 |-  ( A. x e. A ( f ` x ) : B -1-1-> C -> ( y e. T -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B ) )
126 125 imp 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ y e. T ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
127 126 adantrr 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
128 127 adantr 
 |-  ( ( ( 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 )
129 125 ralrimiv 
 |-  ( A. x e. A ( f ` x ) : B -1-1-> C -> A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B )
130 fveq2 
 |-  ( y = z -> ( 2nd ` y ) = ( 2nd ` z ) )
131 fveq2 
 |-  ( y = z -> ( 1st ` y ) = ( 1st ` z ) )
132 131 csbeq1d 
 |-  ( y = z -> [_ ( 1st ` y ) / x ]_ B = [_ ( 1st ` z ) / x ]_ B )
133 130 132 eleq12d 
 |-  ( y = z -> ( ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B <-> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B ) )
134 133 rspccva 
 |-  ( ( A. y e. T ( 2nd ` y ) e. [_ ( 1st ` y ) / x ]_ B /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
135 129 134 sylan 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ z e. T ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
136 135 adantrl 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> ( 2nd ` z ) e. [_ ( 1st ` z ) / x ]_ B )
137 136 adantr 
 |-  ( ( ( 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 )
138 93 csbeq1d 
 |-  ( ( ( 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 )
139 137 138 eleqtrrd 
 |-  ( ( ( 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 )
140 f1fveq 
 |-  ( ( ( 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 ) ) )
141 116 128 139 140 syl12anc 
 |-  ( ( ( 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 ) ) )
142 96 141 bitr3d 
 |-  ( ( ( 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 ) ) )
143 142 pm5.32da 
 |-  ( ( 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 ) ) ) )
144 simprr 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. T )
145 98 144 sselid 
 |-  ( ( A. x e. A ( f ` x ) : B -1-1-> C /\ ( y e. T /\ z e. T ) ) -> z e. ( A X. _V ) )
146 xpopth 
 |-  ( ( y e. ( A X. _V ) /\ z e. ( A X. _V ) ) -> ( ( ( 1st ` y ) = ( 1st ` z ) /\ ( 2nd ` y ) = ( 2nd ` z ) ) <-> y = z ) )
147 100 145 146 syl2anc 
 |-  ( ( 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 ) )
148 143 147 bitrd 
 |-  ( ( 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 ) )
149 92 148 bitrid 
 |-  ( ( 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 ) )
150 149 ex 
 |-  ( 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 89 150 dom2d 
 |-  ( A. x e. A ( f ` x ) : B -1-1-> C -> ( ( A X. C ) e. _V -> T ~<_ ( A X. C ) ) )
152 66 151 syl5com 
 |-  ( ph -> ( A. x e. A ( f ` x ) : B -1-1-> C -> T ~<_ ( A X. C ) ) )
153 49 152 biimtrrid 
 |-  ( ph -> ( A. y e. A ( f ` y ) : [_ y / x ]_ B -1-1-> C -> T ~<_ ( A X. C ) ) )
154 153 adantld 
 |-  ( 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 ) ) )
155 154 exlimdv 
 |-  ( 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 ) ) )
156 39 155 mpd 
 |-  ( ph -> T ~<_ ( A X. C ) )