Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasnopn GIF version

Theorem imasnopn 12527
 Description: If a relation graph is open, then an image set of a singleton is also open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.)
Hypothesis
Ref Expression
imasnopn.1 𝑋 = 𝐽
Assertion
Ref Expression
imasnopn (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑅 “ {𝐴}) ∈ 𝐾)

Proof of Theorem imasnopn
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nfv 1509 . . . 4 𝑦((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋))
2 nfcv 2282 . . . 4 𝑦(𝑅 “ {𝐴})
3 nfrab1 2614 . . . 4 𝑦{𝑦 𝐾 ∣ ⟨𝐴, 𝑦⟩ ∈ 𝑅}
4 txtop 12488 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top)
54adantr 274 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝐽 ×t 𝐾) ∈ Top)
6 simprl 521 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → 𝑅 ∈ (𝐽 ×t 𝐾))
7 eqid 2140 . . . . . . . . . . . . 13 (𝐽 ×t 𝐾) = (𝐽 ×t 𝐾)
87eltopss 12235 . . . . . . . . . . . 12 (((𝐽 ×t 𝐾) ∈ Top ∧ 𝑅 ∈ (𝐽 ×t 𝐾)) → 𝑅 (𝐽 ×t 𝐾))
95, 6, 8syl2anc 409 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → 𝑅 (𝐽 ×t 𝐾))
10 imasnopn.1 . . . . . . . . . . . . 13 𝑋 = 𝐽
11 eqid 2140 . . . . . . . . . . . . 13 𝐾 = 𝐾
1210, 11txuni 12491 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × 𝐾) = (𝐽 ×t 𝐾))
1312adantr 274 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑋 × 𝐾) = (𝐽 ×t 𝐾))
149, 13sseqtrrd 3142 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → 𝑅 ⊆ (𝑋 × 𝐾))
15 imass1 4923 . . . . . . . . . 10 (𝑅 ⊆ (𝑋 × 𝐾) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × 𝐾) “ {𝐴}))
1614, 15syl 14 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑅 “ {𝐴}) ⊆ ((𝑋 × 𝐾) “ {𝐴}))
17 xpimasn 4996 . . . . . . . . . 10 (𝐴𝑋 → ((𝑋 × 𝐾) “ {𝐴}) = 𝐾)
1817ad2antll 483 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → ((𝑋 × 𝐾) “ {𝐴}) = 𝐾)
1916, 18sseqtrd 3141 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑅 “ {𝐴}) ⊆ 𝐾)
2019sseld 3102 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) → 𝑦 𝐾))
2120pm4.71rd 392 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 𝐾𝑦 ∈ (𝑅 “ {𝐴}))))
22 elimasng 4916 . . . . . . . . 9 ((𝐴𝑋𝑦 ∈ V) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ ⟨𝐴, 𝑦⟩ ∈ 𝑅))
2322elvd 2695 . . . . . . . 8 (𝐴𝑋 → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ ⟨𝐴, 𝑦⟩ ∈ 𝑅))
2423ad2antll 483 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ ⟨𝐴, 𝑦⟩ ∈ 𝑅))
2524anbi2d 460 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → ((𝑦 𝐾𝑦 ∈ (𝑅 “ {𝐴})) ↔ (𝑦 𝐾 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝑅)))
2621, 25bitrd 187 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ (𝑦 𝐾 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝑅)))
27 rabid 2610 . . . . 5 (𝑦 ∈ {𝑦 𝐾 ∣ ⟨𝐴, 𝑦⟩ ∈ 𝑅} ↔ (𝑦 𝐾 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝑅))
2826, 27bitr4di 197 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 ∈ (𝑅 “ {𝐴}) ↔ 𝑦 ∈ {𝑦 𝐾 ∣ ⟨𝐴, 𝑦⟩ ∈ 𝑅}))
291, 2, 3, 28eqrd 3121 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑅 “ {𝐴}) = {𝑦 𝐾 ∣ ⟨𝐴, 𝑦⟩ ∈ 𝑅})
30 eqid 2140 . . . 4 (𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) = (𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩)
3130mptpreima 5041 . . 3 ((𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) “ 𝑅) = {𝑦 𝐾 ∣ ⟨𝐴, 𝑦⟩ ∈ 𝑅}
3229, 31eqtr4di 2191 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑅 “ {𝐴}) = ((𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) “ 𝑅))
3311toptopon 12244 . . . . . 6 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
3433biimpi 119 . . . . 5 (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘ 𝐾))
3534ad2antlr 481 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → 𝐾 ∈ (TopOn‘ 𝐾))
3610toptopon 12244 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
3736biimpi 119 . . . . . 6 (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋))
3837ad2antrr 480 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
39 simprr 522 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → 𝐴𝑋)
4035, 38, 39cnmptc 12510 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 𝐾𝐴) ∈ (𝐾 Cn 𝐽))
4135cnmptid 12509 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 𝐾𝑦) ∈ (𝐾 Cn 𝐾))
4235, 40, 41cnmpt1t 12513 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) ∈ (𝐾 Cn (𝐽 ×t 𝐾)))
43 cnima 12448 . . 3 (((𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) ∈ (𝐾 Cn (𝐽 ×t 𝐾)) ∧ 𝑅 ∈ (𝐽 ×t 𝐾)) → ((𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) “ 𝑅) ∈ 𝐾)
4442, 6, 43syl2anc 409 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → ((𝑦 𝐾 ↦ ⟨𝐴, 𝑦⟩) “ 𝑅) ∈ 𝐾)
4532, 44eqeltrd 2217 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴𝑋)) → (𝑅 “ {𝐴}) ∈ 𝐾)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  {crab 2421  Vcvv 2690   ⊆ wss 3077  {csn 3533  ⟨cop 3536  ∪ cuni 3745   ↦ cmpt 3998   × cxp 4546  ◡ccnv 4547   “ cima 4551  ‘cfv 5132  (class class class)co 5783  Topctop 12223  TopOnctopon 12236   Cn ccn 12413   ×t ctx 12480 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-map 6553  df-topgen 12200  df-top 12224  df-topon 12237  df-bases 12269  df-cn 12416  df-cnp 12417  df-tx 12481 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator