Metamath Proof Explorer

Theorem ptcnplem

Description: Lemma for ptcnp . (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses ptcnp.2 
|- K = ( Xt_ ` F )
ptcnp.3 
|- ( ph -> J e. ( TopOn ` X ) )
ptcnp.4 
|- ( ph -> I e. V )
ptcnp.5 
|- ( ph -> F : I --> Top )
ptcnp.6 
|- ( ph -> D e. X )
ptcnp.7 
|- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )
ptcnplem.1 
|- F/ k ps
ptcnplem.2 
|- ( ( ph /\ ps ) -> G Fn I )
ptcnplem.3 
|- ( ( ( ph /\ ps ) /\ k e. I ) -> ( G ` k ) e. ( F ` k ) )
ptcnplem.4 
|- ( ( ph /\ ps ) -> W e. Fin )
ptcnplem.5 
|- ( ( ( ph /\ ps ) /\ k e. ( I \ W ) ) -> ( G ` k ) = U. ( F ` k ) )
ptcnplem.6 
|- ( ( ph /\ ps ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ k e. I ( G ` k ) )
Assertion ptcnplem 
|- ( ( ph /\ ps ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) ) )

Proof

Step Hyp Ref Expression
1 ptcnp.2 
 |-  K = ( Xt_ ` F )
2 ptcnp.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 ptcnp.4 
 |-  ( ph -> I e. V )
4 ptcnp.5 
 |-  ( ph -> F : I --> Top )
5 ptcnp.6 
 |-  ( ph -> D e. X )
6 ptcnp.7 
 |-  ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )
7 ptcnplem.1 
 |-  F/ k ps
8 ptcnplem.2 
 |-  ( ( ph /\ ps ) -> G Fn I )
9 ptcnplem.3 
 |-  ( ( ( ph /\ ps ) /\ k e. I ) -> ( G ` k ) e. ( F ` k ) )
10 ptcnplem.4 
 |-  ( ( ph /\ ps ) -> W e. Fin )
11 ptcnplem.5 
 |-  ( ( ( ph /\ ps ) /\ k e. ( I \ W ) ) -> ( G ` k ) = U. ( F ` k ) )
12 ptcnplem.6 
 |-  ( ( ph /\ ps ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ k e. I ( G ` k ) )
13 inss2 
 |-  ( I i^i W ) C_ W
14 ssfi 
 |-  ( ( W e. Fin /\ ( I i^i W ) C_ W ) -> ( I i^i W ) e. Fin )
15 10 13 14 sylancl 
 |-  ( ( ph /\ ps ) -> ( I i^i W ) e. Fin )
16 nfv 
 |-  F/ k ph
17 16 7 nfan 
 |-  F/ k ( ph /\ ps )
18 elinel1 
 |-  ( k e. ( I i^i W ) -> k e. I )
19 6 adantlr 
 |-  ( ( ( ph /\ ps ) /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )
20 5 adantr 
 |-  ( ( ph /\ ps ) -> D e. X )
21 simpr 
 |-  ( ( ( ph /\ k e. I ) /\ x e. X ) -> x e. X )
22 2 adantr 
 |-  ( ( ph /\ k e. I ) -> J e. ( TopOn ` X ) )
23 4 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. Top )
24 toptopon2 
 |-  ( ( F ` k ) e. Top <-> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
25 23 24 sylib 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
26 cnpf2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) /\ ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) )
27 22 25 6 26 syl3anc 
 |-  ( ( ph /\ k e. I ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) )
28 eqid 
 |-  ( x e. X |-> A ) = ( x e. X |-> A )
29 28 fmpt 
 |-  ( A. x e. X A e. U. ( F ` k ) <-> ( x e. X |-> A ) : X --> U. ( F ` k ) )
30 27 29 sylibr 
 |-  ( ( ph /\ k e. I ) -> A. x e. X A e. U. ( F ` k ) )
31 30 r19.21bi 
 |-  ( ( ( ph /\ k e. I ) /\ x e. X ) -> A e. U. ( F ` k ) )
32 28 fvmpt2 
 |-  ( ( x e. X /\ A e. U. ( F ` k ) ) -> ( ( x e. X |-> A ) ` x ) = A )
33 21 31 32 syl2anc 
 |-  ( ( ( ph /\ k e. I ) /\ x e. X ) -> ( ( x e. X |-> A ) ` x ) = A )
34 33 an32s 
 |-  ( ( ( ph /\ x e. X ) /\ k e. I ) -> ( ( x e. X |-> A ) ` x ) = A )
35 34 mpteq2dva 
 |-  ( ( ph /\ x e. X ) -> ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( k e. I |-> A ) )
36 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
37 3 adantr 
 |-  ( ( ph /\ x e. X ) -> I e. V )
38 37 mptexd 
 |-  ( ( ph /\ x e. X ) -> ( k e. I |-> A ) e. _V )
39 eqid 
 |-  ( x e. X |-> ( k e. I |-> A ) ) = ( x e. X |-> ( k e. I |-> A ) )
40 39 fvmpt2 
 |-  ( ( x e. X /\ ( k e. I |-> A ) e. _V ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) = ( k e. I |-> A ) )
41 36 38 40 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) = ( k e. I |-> A ) )
42 35 41 eqtr4d 
 |-  ( ( ph /\ x e. X ) -> ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) )
43 42 ralrimiva 
 |-  ( ph -> A. x e. X ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) )
44 43 adantr 
 |-  ( ( ph /\ ps ) -> A. x e. X ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) )
45 nfcv 
 |-  F/_ x I
46 nffvmpt1 
 |-  F/_ x ( ( x e. X |-> A ) ` D )
47 45 46 nfmpt 
 |-  F/_ x ( k e. I |-> ( ( x e. X |-> A ) ` D ) )
48 nffvmpt1 
 |-  F/_ x ( ( x e. X |-> ( k e. I |-> A ) ) ` D )
49 47 48 nfeq 
 |-  F/ x ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` D )
50 fveq2 
 |-  ( x = D -> ( ( x e. X |-> A ) ` x ) = ( ( x e. X |-> A ) ` D ) )
51 50 mpteq2dv 
 |-  ( x = D -> ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) )
52 fveq2 
 |-  ( x = D -> ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) )
53 51 52 eqeq12d 
 |-  ( x = D -> ( ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) <-> ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) ) )
54 49 53 rspc 
 |-  ( D e. X -> ( A. x e. X ( k e. I |-> ( ( x e. X |-> A ) ` x ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) -> ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) ) )
55 20 44 54 sylc 
 |-  ( ( ph /\ ps ) -> ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) )
56 55 12 eqeltrd 
 |-  ( ( ph /\ ps ) -> ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) e. X_ k e. I ( G ` k ) )
57 3 adantr 
 |-  ( ( ph /\ ps ) -> I e. V )
58 mptelixpg 
 |-  ( I e. V -> ( ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) e. X_ k e. I ( G ` k ) <-> A. k e. I ( ( x e. X |-> A ) ` D ) e. ( G ` k ) ) )
59 57 58 syl 
 |-  ( ( ph /\ ps ) -> ( ( k e. I |-> ( ( x e. X |-> A ) ` D ) ) e. X_ k e. I ( G ` k ) <-> A. k e. I ( ( x e. X |-> A ) ` D ) e. ( G ` k ) ) )
60 56 59 mpbid 
 |-  ( ( ph /\ ps ) -> A. k e. I ( ( x e. X |-> A ) ` D ) e. ( G ` k ) )
61 60 r19.21bi 
 |-  ( ( ( ph /\ ps ) /\ k e. I ) -> ( ( x e. X |-> A ) ` D ) e. ( G ` k ) )
62 cnpimaex 
 |-  ( ( ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) /\ ( G ` k ) e. ( F ` k ) /\ ( ( x e. X |-> A ) ` D ) e. ( G ` k ) ) -> E. u e. J ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) )
63 19 9 61 62 syl3anc 
 |-  ( ( ( ph /\ ps ) /\ k e. I ) -> E. u e. J ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) )
64 18 63 sylan2 
 |-  ( ( ( ph /\ ps ) /\ k e. ( I i^i W ) ) -> E. u e. J ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) )
65 64 ex 
 |-  ( ( ph /\ ps ) -> ( k e. ( I i^i W ) -> E. u e. J ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) ) )
66 17 65 ralrimi 
 |-  ( ( ph /\ ps ) -> A. k e. ( I i^i W ) E. u e. J ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) )
67 eleq2 
 |-  ( u = ( f ` k ) -> ( D e. u <-> D e. ( f ` k ) ) )
68 imaeq2 
 |-  ( u = ( f ` k ) -> ( ( x e. X |-> A ) " u ) = ( ( x e. X |-> A ) " ( f ` k ) ) )
69 68 sseq1d 
 |-  ( u = ( f ` k ) -> ( ( ( x e. X |-> A ) " u ) C_ ( G ` k ) <-> ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) )
70 67 69 anbi12d 
 |-  ( u = ( f ` k ) -> ( ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) <-> ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) )
71 70 ac6sfi 
 |-  ( ( ( I i^i W ) e. Fin /\ A. k e. ( I i^i W ) E. u e. J ( D e. u /\ ( ( x e. X |-> A ) " u ) C_ ( G ` k ) ) ) -> E. f ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) )
72 15 66 71 syl2anc 
 |-  ( ( ph /\ ps ) -> E. f ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) )
73 2 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> J e. ( TopOn ` X ) )
74 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
75 73 74 syl 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> X = U. J )
76 75 ineq1d 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( X i^i |^| ran f ) = ( U. J i^i |^| ran f ) )
77 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
78 2 77 syl 
 |-  ( ph -> J e. Top )
79 78 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> J e. Top )
80 frn 
 |-  ( f : ( I i^i W ) --> J -> ran f C_ J )
81 80 ad2antrl 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ran f C_ J )
82 15 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( I i^i W ) e. Fin )
83 ffn 
 |-  ( f : ( I i^i W ) --> J -> f Fn ( I i^i W ) )
84 83 ad2antrl 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> f Fn ( I i^i W ) )
85 dffn4 
 |-  ( f Fn ( I i^i W ) <-> f : ( I i^i W ) -onto-> ran f )
86 84 85 sylib 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> f : ( I i^i W ) -onto-> ran f )
87 fofi 
 |-  ( ( ( I i^i W ) e. Fin /\ f : ( I i^i W ) -onto-> ran f ) -> ran f e. Fin )
88 82 86 87 syl2anc 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ran f e. Fin )
89 eqid 
 |-  U. J = U. J
90 89 rintopn 
 |-  ( ( J e. Top /\ ran f C_ J /\ ran f e. Fin ) -> ( U. J i^i |^| ran f ) e. J )
91 79 81 88 90 syl3anc 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( U. J i^i |^| ran f ) e. J )
92 76 91 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( X i^i |^| ran f ) e. J )
93 5 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> D e. X )
94 simpl 
 |-  ( ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) -> D e. ( f ` k ) )
95 94 ralimi 
 |-  ( A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) -> A. k e. ( I i^i W ) D e. ( f ` k ) )
96 95 ad2antll 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. k e. ( I i^i W ) D e. ( f ` k ) )
97 eleq2 
 |-  ( z = ( f ` k ) -> ( D e. z <-> D e. ( f ` k ) ) )
98 97 ralrn 
 |-  ( f Fn ( I i^i W ) -> ( A. z e. ran f D e. z <-> A. k e. ( I i^i W ) D e. ( f ` k ) ) )
99 84 98 syl 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( A. z e. ran f D e. z <-> A. k e. ( I i^i W ) D e. ( f ` k ) ) )
100 96 99 mpbird 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. z e. ran f D e. z )
101 elrint 
 |-  ( D e. ( X i^i |^| ran f ) <-> ( D e. X /\ A. z e. ran f D e. z ) )
102 93 100 101 sylanbrc 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> D e. ( X i^i |^| ran f ) )
103 nfv 
 |-  F/ k f : ( I i^i W ) --> J
104 17 103 nfan 
 |-  F/ k ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J )
105 funmpt 
 |-  Fun ( x e. X |-> A )
106 simp-4l 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ph )
107 106 2 syl 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> J e. ( TopOn ` X ) )
108 simpllr 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> f : ( I i^i W ) --> J )
109 simplr 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> k e. ( I i^i W ) )
110 108 109 ffvelrnd 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( f ` k ) e. J )
111 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ ( f ` k ) e. J ) -> ( f ` k ) C_ X )
112 107 110 111 syl2anc 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( f ` k ) C_ X )
113 109 elin1d 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> k e. I )
114 106 113 30 syl2anc 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> A. x e. X A e. U. ( F ` k ) )
115 dmmptg 
 |-  ( A. x e. X A e. U. ( F ` k ) -> dom ( x e. X |-> A ) = X )
116 114 115 syl 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> dom ( x e. X |-> A ) = X )
117 112 116 sseqtrrd 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( f ` k ) C_ dom ( x e. X |-> A ) )
118 funimass4 
 |-  ( ( Fun ( x e. X |-> A ) /\ ( f ` k ) C_ dom ( x e. X |-> A ) ) -> ( ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) <-> A. t e. ( f ` k ) ( ( x e. X |-> A ) ` t ) e. ( G ` k ) ) )
119 105 117 118 sylancr 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) <-> A. t e. ( f ` k ) ( ( x e. X |-> A ) ` t ) e. ( G ` k ) ) )
120 nffvmpt1 
 |-  F/_ x ( ( x e. X |-> A ) ` t )
121 120 nfel1 
 |-  F/ x ( ( x e. X |-> A ) ` t ) e. ( G ` k )
122 nfv 
 |-  F/ t ( ( x e. X |-> A ) ` x ) e. ( G ` k )
123 fveq2 
 |-  ( t = x -> ( ( x e. X |-> A ) ` t ) = ( ( x e. X |-> A ) ` x ) )
124 123 eleq1d 
 |-  ( t = x -> ( ( ( x e. X |-> A ) ` t ) e. ( G ` k ) <-> ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) )
125 121 122 124 cbvralw 
 |-  ( A. t e. ( f ` k ) ( ( x e. X |-> A ) ` t ) e. ( G ` k ) <-> A. x e. ( f ` k ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) )
126 119 125 bitrdi 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) <-> A. x e. ( f ` k ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) )
127 inss1 
 |-  ( X i^i |^| ran f ) C_ X
128 ssralv 
 |-  ( ( X i^i |^| ran f ) C_ X -> ( A. x e. X A e. U. ( F ` k ) -> A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) ) )
129 127 114 128 mpsyl 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) )
130 inss2 
 |-  ( X i^i |^| ran f ) C_ |^| ran f
131 108 83 syl 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> f Fn ( I i^i W ) )
132 fnfvelrn 
 |-  ( ( f Fn ( I i^i W ) /\ k e. ( I i^i W ) ) -> ( f ` k ) e. ran f )
133 131 109 132 syl2anc 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( f ` k ) e. ran f )
134 intss1 
 |-  ( ( f ` k ) e. ran f -> |^| ran f C_ ( f ` k ) )
135 133 134 syl 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> |^| ran f C_ ( f ` k ) )
136 130 135 sstrid 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( X i^i |^| ran f ) C_ ( f ` k ) )
137 ssralv 
 |-  ( ( X i^i |^| ran f ) C_ ( f ` k ) -> ( A. x e. ( f ` k ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) -> A. x e. ( X i^i |^| ran f ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) )
138 136 137 syl 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( A. x e. ( f ` k ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) -> A. x e. ( X i^i |^| ran f ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) )
139 r19.26 
 |-  ( A. x e. ( X i^i |^| ran f ) ( A e. U. ( F ` k ) /\ ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) <-> ( A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) /\ A. x e. ( X i^i |^| ran f ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) )
140 elinel1 
 |-  ( x e. ( X i^i |^| ran f ) -> x e. X )
141 140 32 sylan 
 |-  ( ( x e. ( X i^i |^| ran f ) /\ A e. U. ( F ` k ) ) -> ( ( x e. X |-> A ) ` x ) = A )
142 141 eleq1d 
 |-  ( ( x e. ( X i^i |^| ran f ) /\ A e. U. ( F ` k ) ) -> ( ( ( x e. X |-> A ) ` x ) e. ( G ` k ) <-> A e. ( G ` k ) ) )
143 142 biimpd 
 |-  ( ( x e. ( X i^i |^| ran f ) /\ A e. U. ( F ` k ) ) -> ( ( ( x e. X |-> A ) ` x ) e. ( G ` k ) -> A e. ( G ` k ) ) )
144 143 expimpd 
 |-  ( x e. ( X i^i |^| ran f ) -> ( ( A e. U. ( F ` k ) /\ ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) -> A e. ( G ` k ) ) )
145 144 ralimia 
 |-  ( A. x e. ( X i^i |^| ran f ) ( A e. U. ( F ` k ) /\ ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
146 139 145 sylbir 
 |-  ( ( A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) /\ A. x e. ( X i^i |^| ran f ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
147 129 138 146 syl6an 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( A. x e. ( f ` k ) ( ( x e. X |-> A ) ` x ) e. ( G ` k ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
148 126 147 sylbid 
 |-  ( ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) /\ D e. ( f ` k ) ) -> ( ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
149 148 expimpd 
 |-  ( ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) /\ k e. ( I i^i W ) ) -> ( ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
150 104 149 ralimdaa 
 |-  ( ( ( ph /\ ps ) /\ f : ( I i^i W ) --> J ) -> ( A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) -> A. k e. ( I i^i W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
151 150 impr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. k e. ( I i^i W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
152 simpl 
 |-  ( ( ph /\ ps ) -> ph )
153 eldifi 
 |-  ( k e. ( I \ W ) -> k e. I )
154 140 31 sylan2 
 |-  ( ( ( ph /\ k e. I ) /\ x e. ( X i^i |^| ran f ) ) -> A e. U. ( F ` k ) )
155 154 ralrimiva 
 |-  ( ( ph /\ k e. I ) -> A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) )
156 152 153 155 syl2an 
 |-  ( ( ( ph /\ ps ) /\ k e. ( I \ W ) ) -> A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) )
157 eleq2 
 |-  ( ( G ` k ) = U. ( F ` k ) -> ( A e. ( G ` k ) <-> A e. U. ( F ` k ) ) )
158 157 ralbidv 
 |-  ( ( G ` k ) = U. ( F ` k ) -> ( A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) <-> A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) ) )
159 11 158 syl 
 |-  ( ( ( ph /\ ps ) /\ k e. ( I \ W ) ) -> ( A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) <-> A. x e. ( X i^i |^| ran f ) A e. U. ( F ` k ) ) )
160 156 159 mpbird 
 |-  ( ( ( ph /\ ps ) /\ k e. ( I \ W ) ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
161 160 ex 
 |-  ( ( ph /\ ps ) -> ( k e. ( I \ W ) -> A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
162 17 161 ralrimi 
 |-  ( ( ph /\ ps ) -> A. k e. ( I \ W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
163 162 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. k e. ( I \ W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
164 inundif 
 |-  ( ( I i^i W ) u. ( I \ W ) ) = I
165 164 raleqi 
 |-  ( A. k e. ( ( I i^i W ) u. ( I \ W ) ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) <-> A. k e. I A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
166 ralunb 
 |-  ( A. k e. ( ( I i^i W ) u. ( I \ W ) ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) <-> ( A. k e. ( I i^i W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) /\ A. k e. ( I \ W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
167 165 166 bitr3i 
 |-  ( A. k e. I A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) <-> ( A. k e. ( I i^i W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) /\ A. k e. ( I \ W ) A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) ) )
168 151 163 167 sylanbrc 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. k e. I A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
169 ralcom 
 |-  ( A. x e. ( X i^i |^| ran f ) A. k e. I A e. ( G ` k ) <-> A. k e. I A. x e. ( X i^i |^| ran f ) A e. ( G ` k ) )
170 168 169 sylibr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. x e. ( X i^i |^| ran f ) A. k e. I A e. ( G ` k ) )
171 3 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> I e. V )
172 nffvmpt1 
 |-  F/_ x ( ( x e. X |-> ( k e. I |-> A ) ) ` t )
173 172 nfel1 
 |-  F/ x ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k )
174 nfv 
 |-  F/ t ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) e. X_ k e. I ( G ` k )
175 fveq2 
 |-  ( t = x -> ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) = ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) )
176 175 eleq1d 
 |-  ( t = x -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) e. X_ k e. I ( G ` k ) ) )
177 173 174 176 cbvralw 
 |-  ( A. t e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) <-> A. x e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) e. X_ k e. I ( G ` k ) )
178 mptexg 
 |-  ( I e. V -> ( k e. I |-> A ) e. _V )
179 140 178 40 syl2anr 
 |-  ( ( I e. V /\ x e. ( X i^i |^| ran f ) ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) = ( k e. I |-> A ) )
180 179 eleq1d 
 |-  ( ( I e. V /\ x e. ( X i^i |^| ran f ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) e. X_ k e. I ( G ` k ) <-> ( k e. I |-> A ) e. X_ k e. I ( G ` k ) ) )
181 mptelixpg 
 |-  ( I e. V -> ( ( k e. I |-> A ) e. X_ k e. I ( G ` k ) <-> A. k e. I A e. ( G ` k ) ) )
182 181 adantr 
 |-  ( ( I e. V /\ x e. ( X i^i |^| ran f ) ) -> ( ( k e. I |-> A ) e. X_ k e. I ( G ` k ) <-> A. k e. I A e. ( G ` k ) ) )
183 180 182 bitrd 
 |-  ( ( I e. V /\ x e. ( X i^i |^| ran f ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) e. X_ k e. I ( G ` k ) <-> A. k e. I A e. ( G ` k ) ) )
184 183 ralbidva 
 |-  ( I e. V -> ( A. x e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` x ) e. X_ k e. I ( G ` k ) <-> A. x e. ( X i^i |^| ran f ) A. k e. I A e. ( G ` k ) ) )
185 177 184 syl5bb 
 |-  ( I e. V -> ( A. t e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) <-> A. x e. ( X i^i |^| ran f ) A. k e. I A e. ( G ` k ) ) )
186 171 185 syl 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( A. t e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) <-> A. x e. ( X i^i |^| ran f ) A. k e. I A e. ( G ` k ) ) )
187 170 186 mpbird 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. t e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) )
188 funmpt 
 |-  Fun ( x e. X |-> ( k e. I |-> A ) )
189 3 mptexd 
 |-  ( ph -> ( k e. I |-> A ) e. _V )
190 189 ralrimivw 
 |-  ( ph -> A. x e. X ( k e. I |-> A ) e. _V )
191 190 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> A. x e. X ( k e. I |-> A ) e. _V )
192 dmmptg 
 |-  ( A. x e. X ( k e. I |-> A ) e. _V -> dom ( x e. X |-> ( k e. I |-> A ) ) = X )
193 191 192 syl 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> dom ( x e. X |-> ( k e. I |-> A ) ) = X )
194 127 193 sseqtrrid 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( X i^i |^| ran f ) C_ dom ( x e. X |-> ( k e. I |-> A ) ) )
195 funimass4 
 |-  ( ( Fun ( x e. X |-> ( k e. I |-> A ) ) /\ ( X i^i |^| ran f ) C_ dom ( x e. X |-> ( k e. I |-> A ) ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) C_ X_ k e. I ( G ` k ) <-> A. t e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) ) )
196 188 194 195 sylancr 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) C_ X_ k e. I ( G ` k ) <-> A. t e. ( X i^i |^| ran f ) ( ( x e. X |-> ( k e. I |-> A ) ) ` t ) e. X_ k e. I ( G ` k ) ) )
197 187 196 mpbird 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) C_ X_ k e. I ( G ` k ) )
198 eleq2 
 |-  ( z = ( X i^i |^| ran f ) -> ( D e. z <-> D e. ( X i^i |^| ran f ) ) )
199 imaeq2 
 |-  ( z = ( X i^i |^| ran f ) -> ( ( x e. X |-> ( k e. I |-> A ) ) " z ) = ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) )
200 199 sseq1d 
 |-  ( z = ( X i^i |^| ran f ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) C_ X_ k e. I ( G ` k ) ) )
201 198 200 anbi12d 
 |-  ( z = ( X i^i |^| ran f ) -> ( ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) ) <-> ( D e. ( X i^i |^| ran f ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) C_ X_ k e. I ( G ` k ) ) ) )
202 201 rspcev 
 |-  ( ( ( X i^i |^| ran f ) e. J /\ ( D e. ( X i^i |^| ran f ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) " ( X i^i |^| ran f ) ) C_ X_ k e. I ( G ` k ) ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) ) )
203 92 102 197 202 syl12anc 
 |-  ( ( ( ph /\ ps ) /\ ( f : ( I i^i W ) --> J /\ A. k e. ( I i^i W ) ( D e. ( f ` k ) /\ ( ( x e. X |-> A ) " ( f ` k ) ) C_ ( G ` k ) ) ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) ) )
204 72 203 exlimddv 
 |-  ( ( ph /\ ps ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) ) )