Metamath Proof Explorer

Theorem cnmptre

Description: Lemma for iirevcn and related functions. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypotheses cnmptre.1 
|- R = ( TopOpen ` CCfld )
cnmptre.2 
|- J = ( ( topGen ` ran (,) ) |`t A )
cnmptre.3 
|- K = ( ( topGen ` ran (,) ) |`t B )
cnmptre.4 
|- ( ph -> A C_ RR )
cnmptre.5 
|- ( ph -> B C_ RR )
cnmptre.6 
|- ( ( ph /\ x e. A ) -> F e. B )
cnmptre.7 
|- ( ph -> ( x e. CC |-> F ) e. ( R Cn R ) )
Assertion cnmptre 
|- ( ph -> ( x e. A |-> F ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 cnmptre.1 
 |-  R = ( TopOpen ` CCfld )
2 cnmptre.2 
 |-  J = ( ( topGen ` ran (,) ) |`t A )
3 cnmptre.3 
 |-  K = ( ( topGen ` ran (,) ) |`t B )
4 cnmptre.4 
 |-  ( ph -> A C_ RR )
5 cnmptre.5 
 |-  ( ph -> B C_ RR )
6 cnmptre.6 
 |-  ( ( ph /\ x e. A ) -> F e. B )
7 cnmptre.7 
 |-  ( ph -> ( x e. CC |-> F ) e. ( R Cn R ) )
8 eqid 
 |-  ( R |`t A ) = ( R |`t A )
9 1 cnfldtopon 
 |-  R e. ( TopOn ` CC )
10 9 a1i 
 |-  ( ph -> R e. ( TopOn ` CC ) )
11 ax-resscn 
 |-  RR C_ CC
12 4 11 sstrdi 
 |-  ( ph -> A C_ CC )
13 8 10 12 7 cnmpt1res 
 |-  ( ph -> ( x e. A |-> F ) e. ( ( R |`t A ) Cn R ) )
14 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
15 1 14 rerest 
 |-  ( A C_ RR -> ( R |`t A ) = ( ( topGen ` ran (,) ) |`t A ) )
16 4 15 syl 
 |-  ( ph -> ( R |`t A ) = ( ( topGen ` ran (,) ) |`t A ) )
17 16 2 eqtr4di 
 |-  ( ph -> ( R |`t A ) = J )
18 17 oveq1d 
 |-  ( ph -> ( ( R |`t A ) Cn R ) = ( J Cn R ) )
19 13 18 eleqtrd 
 |-  ( ph -> ( x e. A |-> F ) e. ( J Cn R ) )
20 6 fmpttd 
 |-  ( ph -> ( x e. A |-> F ) : A --> B )
21 20 frnd 
 |-  ( ph -> ran ( x e. A |-> F ) C_ B )
22 5 11 sstrdi 
 |-  ( ph -> B C_ CC )
23 cnrest2 
 |-  ( ( R e. ( TopOn ` CC ) /\ ran ( x e. A |-> F ) C_ B /\ B C_ CC ) -> ( ( x e. A |-> F ) e. ( J Cn R ) <-> ( x e. A |-> F ) e. ( J Cn ( R |`t B ) ) ) )
24 9 21 22 23 mp3an2i 
 |-  ( ph -> ( ( x e. A |-> F ) e. ( J Cn R ) <-> ( x e. A |-> F ) e. ( J Cn ( R |`t B ) ) ) )
25 19 24 mpbid 
 |-  ( ph -> ( x e. A |-> F ) e. ( J Cn ( R |`t B ) ) )
26 1 14 rerest 
 |-  ( B C_ RR -> ( R |`t B ) = ( ( topGen ` ran (,) ) |`t B ) )
27 5 26 syl 
 |-  ( ph -> ( R |`t B ) = ( ( topGen ` ran (,) ) |`t B ) )
28 27 3 eqtr4di 
 |-  ( ph -> ( R |`t B ) = K )
29 28 oveq2d 
 |-  ( ph -> ( J Cn ( R |`t B ) ) = ( J Cn K ) )
30 25 29 eleqtrd 
 |-  ( ph -> ( x e. A |-> F ) e. ( J Cn K ) )