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 28 difexd 
 |-  ( D e. ( *Met ` X ) -> ( X \ ( M ` k ) ) e. _V )
30 29 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( X \ ( M ` k ) ) e. _V )
31 fveq2 
 |-  ( x = k -> ( M ` x ) = ( M ` k ) )
32 31 difeq2d 
 |-  ( x = k -> ( X \ ( M ` x ) ) = ( X \ ( M ` k ) ) )
33 eqid 
 |-  ( x e. NN |-> ( X \ ( M ` x ) ) ) = ( x e. NN |-> ( X \ ( M ` x ) ) )
34 32 33 fvmptg 
 |-  ( ( k e. NN /\ ( X \ ( M ` k ) ) e. _V ) -> ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = ( X \ ( M ` k ) ) )
35 27 30 34 syl2anr 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = ( X \ ( M ` k ) ) )
36 15 difeq1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( X \ ( M ` k ) ) = ( U. J \ ( M ` k ) ) )
37 35 36 eqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) = ( U. J \ ( M ` k ) ) )
38 37 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 ) ) ) )
39 26 38 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 ) ) )
40 39 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 ) ) = (/) ) )
41 19 40 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 ) ) = (/) ) )
42 16 41 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 ) ) = (/) ) )
43 42 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 ) ) = (/) ) )
44 4 43 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 ) ) = (/) ) )
45 ffvelrn 
 |-  ( ( M : NN --> J /\ x e. NN ) -> ( M ` x ) e. J )
46 14 difeq1d 
 |-  ( D e. ( *Met ` X ) -> ( X \ ( M ` x ) ) = ( U. J \ ( M ` x ) ) )
47 46 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ ( M ` x ) e. J ) -> ( X \ ( M ` x ) ) = ( U. J \ ( M ` x ) ) )
48 11 opncld 
 |-  ( ( J e. Top /\ ( M ` x ) e. J ) -> ( U. J \ ( M ` x ) ) e. ( Clsd ` J ) )
49 5 48 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ ( M ` x ) e. J ) -> ( U. J \ ( M ` x ) ) e. ( Clsd ` J ) )
50 47 49 eqeltrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( M ` x ) e. J ) -> ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
51 45 50 sylan2 
 |-  ( ( D e. ( *Met ` X ) /\ ( M : NN --> J /\ x e. NN ) ) -> ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
52 51 anassrs 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ x e. NN ) -> ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
53 52 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> A. x e. NN ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
54 4 53 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> A. x e. NN ( X \ ( M ` x ) ) e. ( Clsd ` J ) )
55 33 fmpt 
 |-  ( A. x e. NN ( X \ ( M ` x ) ) e. ( Clsd ` J ) <-> ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) )
56 54 55 sylib 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( x e. NN |-> ( X \ ( M ` x ) ) ) : NN --> ( Clsd ` J ) )
57 nne 
 |-  ( -. ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) =/= (/) <-> ( ( int ` J ) ` ( ( x e. NN |-> ( X \ ( M ` x ) ) ) ` k ) ) = (/) )
58 57 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 ) ) = (/) )
59 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 ) ) =/= (/) )
60 58 59 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 ) ) =/= (/) )
61 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 ) ) =/= (/) )
62 61 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 ) ) =/= (/) ) )
63 62 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 ) ) ) ) = (/) ) )
64 60 63 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 ) ) ) ) = (/) ) )
65 56 64 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 ) ) ) ) = (/) ) )
66 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 \ (/) ) )
67 28 difexd 
 |-  ( D e. ( *Met ` X ) -> ( X \ ( M ` x ) ) e. _V )
68 67 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ x e. NN ) -> ( X \ ( M ` x ) ) e. _V )
69 68 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> A. x e. NN ( X \ ( M ` x ) ) e. _V )
70 33 fnmpt 
 |-  ( A. x e. NN ( X \ ( M ` x ) ) e. _V -> ( x e. NN |-> ( X \ ( M ` x ) ) ) Fn NN )
71 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 ) ) ) )
72 69 70 71 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 ) ) ) )
73 35 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 ) ) )
74 32 cbviunv 
 |-  U_ x e. NN ( X \ ( M ` x ) ) = U_ k e. NN ( X \ ( M ` k ) )
75 73 74 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 ) ) )
76 72 75 eqtr3d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) = U_ x e. NN ( X \ ( M ` x ) ) )
77 iundif2 
 |-  U_ x e. NN ( X \ ( M ` x ) ) = ( X \ |^|_ x e. NN ( M ` x ) )
78 76 77 eqtrdi 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) = ( X \ |^|_ x e. NN ( M ` x ) ) )
79 ffn 
 |-  ( M : NN --> J -> M Fn NN )
80 79 adantl 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> M Fn NN )
81 fniinfv 
 |-  ( M Fn NN -> |^|_ x e. NN ( M ` x ) = |^| ran M )
82 80 81 syl 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^|_ x e. NN ( M ` x ) = |^| ran M )
83 82 difeq2d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( X \ |^|_ x e. NN ( M ` x ) ) = ( X \ |^| ran M ) )
84 14 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> X = U. J )
85 84 difeq1d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( X \ |^| ran M ) = ( U. J \ |^| ran M ) )
86 78 83 85 3eqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) = ( U. J \ |^| ran M ) )
87 86 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = ( ( int ` J ) ` ( U. J \ |^| ran M ) ) )
88 87 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 ) ) ) )
89 5 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> J e. Top )
90 1nn 
 |-  1 e. NN
91 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 ) ) )
92 fnfvelrn 
 |-  ( ( M Fn NN /\ k e. NN ) -> ( M ` k ) e. ran M )
93 80 92 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> ( M ` k ) e. ran M )
94 intss1 
 |-  ( ( M ` k ) e. ran M -> |^| ran M C_ ( M ` k ) )
95 93 94 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> |^| ran M C_ ( M ` k ) )
96 95 10 sstrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ M : NN --> J ) /\ k e. NN ) -> |^| ran M C_ U. J )
97 96 expcom 
 |-  ( k e. NN -> ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J ) )
98 91 97 vtoclga 
 |-  ( 1 e. NN -> ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J ) )
99 90 98 ax-mp 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> |^| ran M C_ U. J )
100 11 clsval2 
 |-  ( ( J e. Top /\ |^| ran M C_ U. J ) -> ( ( cls ` J ) ` |^| ran M ) = ( U. J \ ( ( int ` J ) ` ( U. J \ |^| ran M ) ) ) )
101 89 99 100 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( cls ` J ) ` |^| ran M ) = ( U. J \ ( ( int ` J ) ` ( U. J \ |^| ran M ) ) ) )
102 88 101 eqtr4d 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( U. J \ ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) ) = ( ( cls ` J ) ` |^| ran M ) )
103 dif0 
 |-  ( U. J \ (/) ) = U. J
104 103 84 eqtr4id 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( U. J \ (/) ) = X )
105 102 104 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 ) )
106 66 105 syl5ib 
 |-  ( ( D e. ( *Met ` X ) /\ M : NN --> J ) -> ( ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) -> ( ( cls ` J ) ` |^| ran M ) = X ) )
107 4 106 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( ( ( int ` J ) ` U. ran ( x e. NN |-> ( X \ ( M ` x ) ) ) ) = (/) -> ( ( cls ` J ) ` |^| ran M ) = X ) )
108 44 65 107 3syld 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J ) -> ( A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X -> ( ( cls ` J ) ` |^| ran M ) = X ) )
109 108 3impia 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> J /\ A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X ) -> ( ( cls ` J ) ` |^| ran M ) = X )