Theorem iscn 23191

Description: The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
iscn	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))

Distinct variable groups:   𝑦,𝐽   𝑦,𝐾   𝑦,𝑋   𝑦,𝐹   𝑦,𝑌

Proof of Theorem iscn

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnfval 23189	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 Cn 𝐾) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽})
2	1	eleq2d 2823	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽}))
3		cnveq 5830	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
4	3	imaeq1d 6026	. . . . . 6 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ 𝑦) = (◡𝐹 “ 𝑦))
5	4	eleq1d 2822	. . . . 5 ⊢ (𝑓 = 𝐹 → ((◡𝑓 “ 𝑦) ∈ 𝐽 ↔ (◡𝐹 “ 𝑦) ∈ 𝐽))
6	5	ralbidv 3161	. . . 4 ⊢ (𝑓 = 𝐹 → (∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽 ↔ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽))
7	6	elrab 3648	. . 3 ⊢ (𝐹 ∈ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽} ↔ (𝐹 ∈ (𝑌 ↑m 𝑋) ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽))
8		toponmax 22882	. . . . 5 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
9		toponmax 22882	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
10		elmapg 8788	. . . . 5 ⊢ ((𝑌 ∈ 𝐾 ∧ 𝑋 ∈ 𝐽) → (𝐹 ∈ (𝑌 ↑m 𝑋) ↔ 𝐹:𝑋⟶𝑌))
11	8, 9, 10	syl2anr 598	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑌 ↑m 𝑋) ↔ 𝐹:𝑋⟶𝑌))
12	11	anbi1d 632	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ((𝐹 ∈ (𝑌 ↑m 𝑋) ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))
13	7, 12	bitrid 283	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽} ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))
14	2, 13	bitrd 279	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3401  ^◡ccnv 5631   “ cima 5635  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368   ↑_m cmap 8775  TopOnctopon 22866   Cn ccn 23180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777  df-top 22850  df-topon 22867  df-cn 23183

This theorem is referenced by:  iscn2  23194  cnf2  23205  tgcn  23208  ssidcn  23211  iscncl  23225  cnntr  23231  cnss1  23232  cnss2  23233  cncnp  23236  cnrest  23241  cnrest2  23242  cndis  23247  cnindis  23248  kgencn  23512  kgencn3  23514  tx1cn  23565  tx2cn  23566  txdis1cn  23591  qtopid  23661  qtopcn  23670  qtopf1  23772  qustgplem  24077  ucncn  24240  cvmlift2lem9a  35516  rfcnpre1  45376  0cnf  46232