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 fld
cnmptre.2 J = topGen ran . 𝑡 A
cnmptre.3 K = topGen ran . 𝑡 B
cnmptre.4 φ A
cnmptre.5 φ B
cnmptre.6 φ x A F B
cnmptre.7 φ x F R Cn R
Assertion cnmptre φ x A F J Cn K

Proof

Step Hyp Ref Expression
1 cnmptre.1 R = TopOpen fld
2 cnmptre.2 J = topGen ran . 𝑡 A
3 cnmptre.3 K = topGen ran . 𝑡 B
4 cnmptre.4 φ A
5 cnmptre.5 φ B
6 cnmptre.6 φ x A F B
7 cnmptre.7 φ x F R Cn R
8 eqid R 𝑡 A = R 𝑡 A
9 1 cnfldtopon R TopOn
10 9 a1i φ R TopOn
11 ax-resscn
12 4 11 sstrdi φ A
13 8 10 12 7 cnmpt1res φ x A F R 𝑡 A Cn R
14 eqid topGen ran . = topGen ran .
15 1 14 rerest A R 𝑡 A = topGen ran . 𝑡 A
16 4 15 syl φ R 𝑡 A = topGen ran . 𝑡 A
17 16 2 eqtr4di φ R 𝑡 A = J
18 17 oveq1d φ R 𝑡 A Cn R = J Cn R
19 13 18 eleqtrd φ x A F J Cn R
20 6 fmpttd φ x A F : A B
21 20 frnd φ ran x A F B
22 5 11 sstrdi φ B
23 cnrest2 R TopOn ran x A F B B x A F J Cn R x A F J Cn R 𝑡 B
24 9 21 22 23 mp3an2i φ x A F J Cn R x A F J Cn R 𝑡 B
25 19 24 mpbid φ x A F J Cn R 𝑡 B
26 1 14 rerest B R 𝑡 B = topGen ran . 𝑡 B
27 5 26 syl φ R 𝑡 B = topGen ran . 𝑡 B
28 27 3 eqtr4di φ R 𝑡 B = K
29 28 oveq2d φ J Cn R 𝑡 B = J Cn K
30 25 29 eleqtrd φ x A F J Cn K