This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnrest2

Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnrest2 ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
2 1 a1i ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top ) )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
5 3 4 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
6 5 ffnd ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 Fn ∪ 𝐽 )
7 6 a1i ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 Fn ∪ 𝐽 ) )
8 simp2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ran 𝐹 ⊆ 𝐵 )
9 7 8 jctird ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 ⊆ 𝐵 ) ) )
10 df-f ⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝐵 ↔ ( 𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 ⊆ 𝐵 ) )
11 9 10 imbitrrdi ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) )
12 2 11 jcad ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) )
13 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → 𝐽 ∈ Top )
14 13 adantl ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐽 ∈ Top )
15 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
16 14 15 sylib ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
17 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) )
18 17 3adant2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) )
19 18 adantr ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) )
20 simpr ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) )
21 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝐵 )
22 16 19 20 21 syl3anc ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝐵 )
23 14 22 jca ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) )
24 23 ex ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) )
25 vex ⊢ 𝑥 ∈ V
26 25 inex1 ⊢ ( 𝑥 ∩ 𝐵 ) ∈ V
27 26 a1i ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 ∩ 𝐵 ) ∈ V )
28 simpl1 ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
29 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
30 28 29 syl ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝑌 ∈ 𝐾 )
31 simpl3 ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐵 ⊆ 𝑌 )
32 30 31 ssexd ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐵 ∈ V )
33 elrest ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ V ) → ( 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐾 𝑦 = ( 𝑥 ∩ 𝐵 ) ) )
34 28 32 33 syl2anc ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐾 𝑦 = ( 𝑥 ∩ 𝐵 ) ) )
35 imaeq2 ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) )
36 35 eleq1d ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) ∈ 𝐽 ) )
37 36 adantl ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑦 = ( 𝑥 ∩ 𝐵 ) ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) ∈ 𝐽 ) )
38 27 34 37 ralxfr2d ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) ∈ 𝐽 ) )
39 simplrr ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝐵 )
40 ffun ⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝐵 → Fun 𝐹 )
41 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
42 39 40 41 3syl ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
43 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
44 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
45 43 44 sseqtrri ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 )
46 simpll2 ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ran 𝐹 ⊆ 𝐵 )
47 imass2 ⊢ ( ran 𝐹 ⊆ 𝐵 → ( ◡ 𝐹 “ ran 𝐹 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
48 46 47 syl ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ ran 𝐹 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
49 45 48 sstrid ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
50 dfss2 ⊢ ( ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) ↔ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
51 49 50 sylib ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
52 42 51 eqtrd ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
53 52 eleq1d ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
54 53 ralbidva ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ ( 𝑥 ∩ 𝐵 ) ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
55 simprr ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝐵 )
56 55 31 fssd ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
57 56 biantrurd ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
58 38 54 57 3bitrrd ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ↔ ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
59 55 biantrurd ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
60 58 59 bitrd ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
61 simprl ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐽 ∈ Top )
62 61 15 sylib ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
63 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
64 62 28 63 syl2anc ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
65 18 adantr ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) )
66 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
67 62 65 66 syl2anc ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 ↾t 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
68 60 64 67 3bitr4d ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) )
69 68 ex ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 ⟶ 𝐵 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) ) )
70 12 24 69 pm5.21ndd ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) )