Metamath Proof Explorer

Theorem bcth3

Description: Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014)

Ref Expression
Hypothesis bcth.2 
|- J = ( MetOpen ` D )
Assertion bcth3 
|- ( ( D e. ( CMet ` X ) /\ M : NN --> J /\ A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X ) -> ( ( cls ` J ) ` |^| ran M ) = X )

Proof

Step Hyp Ref Expression
1 bcth.2 
 |-  J = ( MetOpen ` D )
2 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
3 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
4 2 3 syl 
 |-  ( D e. ( CMet ` X ) -> D e. ( *Met ` X ) )
5 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
6 5 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> J e. Top )
7 ffvelrn 
 |-  ( ( M : NN --> J /\ k e. NN ) -> ( M ` k ) e. J )
8 elssuni 
 |-  ( ( M ` k ) e. J -> ( M ` k ) C_ U. J )
9 7 8 syl 
 |-  ( ( M : NN --> J /\ k e. NN ) -> ( M ` k ) C_ U. J )
10 9 adantll 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( M ` k ) C_ U. J )
11 eqid 
 |-  U. J = U. J
12 11 clsval2 
 |-  ( ( J e. Top /\ ( M ` k ) C_ U. J ) -> ( ( cls ` J ) ` ( M ` k ) ) = ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) )
13 6 10 12 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( cls ` J ) ` ( M ` k ) ) = ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) )
14 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
15 14 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> X = U. J )
16 13 15 eqeq12d 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( ( cls ` J ) ` ( M ` k ) ) = X <-> ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) = U. J ) )
17 difeq2 
 |-  ( ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) = U. J -> ( U. J \ ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) ) = ( U. J \ U. J ) )
18 difid 
 |-  ( U. J \ U. J ) = (/)
19 17 18 eqtrdi 
 |-  ( ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) = U. J -> ( U. J \ ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) ) = (/) )
20 difss 
 |-  ( U. J \ ( M ` k ) ) C_ U. J
21 11 ntropn 
 |-  ( ( J e. Top /\ ( U. J \ ( M ` k ) ) C_ U. J ) -> ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) e. J )
22 6 20 21 sylancl 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) e. J )
23 elssuni 
 |-  ( ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) e. J -> ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) C_ U. J )
24 22 23 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) C_ U. J )
25 dfss4 
 |-  ( ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) C_ U. J <-> ( U. J \ ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) ) = ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) )
26 24 25 sylib 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( U. J \ ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) ) = ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) )
27 id 
 |-  ( k e. NN -> k e. NN )
28 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
29 difexg 
 |-  ( X e. dom *Met -> ( X \ ( M ` k ) ) e. _V )
30 28 29 syl 
 |-  ( D e. ( *Met ` X ) -> ( X \ ( M ` k ) ) e. _V )
31 30 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( X \ ( M ` k ) ) e. _V )
32 fveq2 
 |-  ( x = k -> ( M ` x ) = ( M ` k ) )
33 32 difeq2d 
 |-  ( x = k -> ( X \ ( M ` x ) ) = ( X \ ( M ` k ) ) )
34 eqid 
 |-  ( x e. NN |-> ( X \ ( M ` x ) ) ) = ( x e. NN |-> ( X \ ( M ` x ) ) )
35 33 34 fvmptg 
 |-  ( ( k e. NN /\ ( X \ ( M ` k ) ) e. _V ) -> ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = ( X \ ( M ` k ) ) )
36 27 31 35 syl2anr 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = ( X \ ( M ` k ) ) )
37 15 difeq1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( X \ ( M ` k ) ) = ( U. J \ ( M ` k ) ) )
38 36 37 eqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = ( U. J \ ( M ` k ) ) )
39 38 fveq2d 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) )
40 26 39 eqtr4d 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( U. J \ ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) ) = ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) )
41 40 eqeq1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( U. J \ ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) ) = (/) <-> ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) ) )
42 19 41 syl5ib 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( U. J \ ( ( int ` J ) ` ( U. J \ ( M ` k ) ) ) ) = U. J -> ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) ) )
43 16 42 sylbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( ( cls ` J ) ` ( M ` k ) ) = X -> ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) ) )
44 43 ralimdva 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X -> A. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) ) )
45 4 44 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X -> A. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) ) )
46 ffvelrn 
 |-  ( ( M : NN --> J /\ x e. NN ) -> ( M ` x ) e. J )
47 14 difeq1d 
 |-  ( D e. ( *Met ` X ) -> ( X \ ( M ` x ) ) = ( U. J \ ( M ` x ) ) )
48 47 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ ( M ` x ) e. J ) -> ( X \ ( M ` x ) ) = ( U. J \ ( M ` x ) ) )
49 11 opncld 
 |-  ( ( J e. Top /\ ( M ` x ) e. J ) -> ( U. J \ ( M ` x ) ) e. ( Clsd ` J ) )
50 5 49 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ ( M ` x ) e. J ) -> ( U. J \ ( M ` x ) ) e. ( Clsd ` J ) )
51 48 50 eqeltrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( M ` x ) e. J ) -> ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
52 46 51 sylan2 
 |-  ( ( D e. ( *Met ` X ) /\ ( M : NN --> J /\ x e. NN ) ) -> ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
53 52 anassrs 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ x e. NN ) -> ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
54 53 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> A. x e. NN ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
55 4 54 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> A. x e. NN ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
56 34 fmpt 
 |-  ( A. x e. NN ( X \ ( M ` x ) ) e. ( Clsd ` J ) <-> ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) )
57 55 56 sylib 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) )
58 nne 
 |-  ( -. ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) <-> ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) )
59 58 ralbii 
 |-  ( A. k e. NN -. ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) <-> A. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) )
60 ralnex 
 |-  ( A. k e. NN -. ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) <-> -. E. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) )
61 59 60 bitr3i 
 |-  ( A. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) <-> -. E. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) )
62 1 bcth 
 |-  ( ( D e. ( CMet ` X ) /\ ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) /\ ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) =/= (/) ) -> E. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) )
63 62 3expia 
 |-  ( ( D e. ( CMet ` X ) /\ ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) ) -> ( ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) =/= (/) -> E. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) ) )
64 63 necon1bd 
 |-  ( ( D e. ( CMet ` X ) /\ ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) ) -> ( -. E. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) -> ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) ) )
65 61 64 syl5bi 
 |-  ( ( D e. ( CMet ` X ) /\ ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) ) -> ( A. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) -> ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) ) )
66 57 65 syldan 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( A. k e. NN ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) -> ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) ) )
67 difeq2 
 |-  ( ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) -> ( U. J \ ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) ) = ( U. J \ (/) ) )
68 difexg 
 |-  ( X e. dom *Met -> ( X \ ( M ` x ) ) e. _V )
69 28 68 syl 
 |-  ( D e. ( *Met ` X ) -> ( X \ ( M ` x ) ) e. _V )
70 69 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ x e. NN ) -> ( X \ ( M ` x ) ) e. _V )
71 70 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> A. x e. NN ( X \ ( M ` x ) ) e. _V )
72 34 fnmpt 
 |-  ( A. x e. NN ( X \ ( M ` x ) ) e. _V -> ( x e. NN |-> ( X \ ( M ` x ) ) ) Fn NN )
73 fniunfv 
 |-  ( ( x e. NN |-> ( X \ ( M ` x ) ) ) Fn NN -> U_ k e. NN ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) )
74 71 72 73 3syl 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U_ k e. NN ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) )
75 36 iuneq2dv 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U_ k e. NN ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = U_ k e. NN ( X \ ( M ` k ) ) )
76 33 cbviunv 
 |-  U_ x e. NN ( X \ ( M ` x ) ) = U_ k e. NN ( X \ ( M ` k ) )
77 75 76 eqtr4di 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U_ k e. NN ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = U_ x e. NN ( X \ ( M ` x ) ) )
78 74 77 eqtr3d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) = U_ x e. NN ( X \ ( M ` x ) ) )
79 iundif2 
 |-  U_ x e. NN ( X \ ( M ` x ) ) = ( X \ |^|_ x e. NN ( M ` x ) )
80 78 79 eqtrdi 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) = ( X \ |^|_ x e. NN ( M ` x ) ) )
81 ffn 
 |-  ( M : NN --> J -> M Fn NN )
82 81 adantl 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> M Fn NN )
83 fniinfv 
 |-  ( M Fn NN -> |^|_ x e. NN ( M ` x ) = |^| ran M )
84 82 83 syl 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^|_ x e. NN ( M ` x ) = |^| ran M )
85 84 difeq2d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( X \ |^|_ x e. NN ( M ` x ) ) = ( X \ |^| ran M ) )
86 14 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> X = U. J )
87 86 difeq1d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( X \ |^| ran M ) = ( U. J \ |^| ran M ) )
88 80 85 87 3eqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) = ( U. J \ |^| ran M ) )
89 88 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = ( ( int ` J ) ` ( U. J \ |^| ran M ) ) )
90 89 difeq2d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( U. J \ ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) ) = ( U. J \ ( ( int ` J ) ` ( U. J \ |^| ran M ) ) ) )
91 5 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> J e. Top )
92 1nn 
 |-  1 e. NN
93 biidd 
 |-  ( k = 1 -> ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J ) <-> ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J ) ) )
94 fnfvelrn 
 |-  ( ( M Fn NN /\ k e. NN ) -> ( M ` k ) e. ran M )
95 82 94 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( M ` k ) e. ran M )
96 intss1 
 |-  ( ( M ` k ) e. ran M -> |^| ran M C_ ( M ` k ) )
97 95 96 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> |^| ran M C_ ( M ` k ) )
98 97 10 sstrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> |^| ran M C_ U. J )
99 98 expcom 
 |-  ( k e. NN -> ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J ) )
100 93 99 vtoclga 
 |-  ( 1 e. NN -> ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J ) )
101 92 100 ax-mp 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J )
102 11 clsval2 
 |-  ( ( J e. Top /\ |^| ran M C_ U. J ) -> ( ( cls ` J ) ` |^| ran M ) = ( U. J \ ( ( int ` J ) ` ( U. J \ |^| ran M ) ) ) )
103 91 101 102 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( cls ` J ) ` |^| ran M ) = ( U. J \ ( ( int ` J ) ` ( U. J \ |^| ran M ) ) ) )
104 90 103 eqtr4d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( U. J \ ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) ) = ( ( cls ` J ) ` |^| ran M ) )
105 dif0 
 |-  ( U. J \ (/) ) = U. J
106 105 86 eqtr4id 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( U. J \ (/) ) = X )
107 104 106 eqeq12d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( U. J \ ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) ) = ( U. J \ (/) ) <-> ( ( cls ` J ) ` |^| ran M ) = X ) )
108 67 107 syl5ib 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) -> ( ( cls ` J ) ` |^| ran M ) = X ) )
109 4 108 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) -> ( ( cls ` J ) ` |^| ran M ) = X ) )
110 45 66 109 3syld 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X -> ( ( cls ` J ) ` |^| ran M ) = X ) )
111 110 3impia 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J /\ A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X ) -> ( ( cls ` J ) ` |^| ran M ) = X )