MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgrest Structured version   Visualization version   GIF version

Theorem tgrest 23188
Description: A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
Assertion
Ref Expression
tgrest ((𝐵𝑉𝐴𝑊) → (topGen‘(𝐵t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴))

Proof of Theorem tgrest
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 7481 . . . . 5 (𝐵t 𝐴) ∈ V
2 eltg3 22990 . . . . 5 ((𝐵t 𝐴) ∈ V → (𝑥 ∈ (topGen‘(𝐵t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦)))
31, 2ax-mp 5 . . . 4 (𝑥 ∈ (topGen‘(𝐵t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦))
4 simpll 766 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝐵𝑉)
5 funmpt 6616 . . . . . . . . . 10 Fun (𝑥𝐵 ↦ (𝑥𝐴))
65a1i 11 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → Fun (𝑥𝐵 ↦ (𝑥𝐴)))
7 restval 17486 . . . . . . . . . . . 12 ((𝐵𝑉𝐴𝑊) → (𝐵t 𝐴) = ran (𝑥𝐵 ↦ (𝑥𝐴)))
87sseq2d 4041 . . . . . . . . . . 11 ((𝐵𝑉𝐴𝑊) → (𝑦 ⊆ (𝐵t 𝐴) ↔ 𝑦 ⊆ ran (𝑥𝐵 ↦ (𝑥𝐴))))
98biimpa 476 . . . . . . . . . 10 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝑦 ⊆ ran (𝑥𝐵 ↦ (𝑥𝐴)))
10 vex 3492 . . . . . . . . . . . . 13 𝑥 ∈ V
1110inex1 5335 . . . . . . . . . . . 12 (𝑥𝐴) ∈ V
1211rgenw 3071 . . . . . . . . . . 11 𝑥𝐵 (𝑥𝐴) ∈ V
13 eqid 2740 . . . . . . . . . . . 12 (𝑥𝐵 ↦ (𝑥𝐴)) = (𝑥𝐵 ↦ (𝑥𝐴))
1413fnmpt 6720 . . . . . . . . . . 11 (∀𝑥𝐵 (𝑥𝐴) ∈ V → (𝑥𝐵 ↦ (𝑥𝐴)) Fn 𝐵)
15 fnima 6710 . . . . . . . . . . 11 ((𝑥𝐵 ↦ (𝑥𝐴)) Fn 𝐵 → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵) = ran (𝑥𝐵 ↦ (𝑥𝐴)))
1612, 14, 15mp2b 10 . . . . . . . . . 10 ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵) = ran (𝑥𝐵 ↦ (𝑥𝐴))
179, 16sseqtrrdi 4060 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝑦 ⊆ ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵))
18 ssimaexg 7008 . . . . . . . . 9 ((𝐵𝑉 ∧ Fun (𝑥𝐵 ↦ (𝑥𝐴)) ∧ 𝑦 ⊆ ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵)) → ∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)))
194, 6, 17, 18syl3anc 1371 . . . . . . . 8 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → ∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)))
20 df-ima 5713 . . . . . . . . . . . . . . . . 17 ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ran ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧)
21 resmpt 6066 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐵 → ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧) = (𝑥𝑧 ↦ (𝑥𝐴)))
2221adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧) = (𝑥𝑧 ↦ (𝑥𝐴)))
2322rneqd 5963 . . . . . . . . . . . . . . . . 17 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ran ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧) = ran (𝑥𝑧 ↦ (𝑥𝐴)))
2420, 23eqtrid 2792 . . . . . . . . . . . . . . . 16 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ran (𝑥𝑧 ↦ (𝑥𝐴)))
2524unieqd 4944 . . . . . . . . . . . . . . 15 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ran (𝑥𝑧 ↦ (𝑥𝐴)))
2611dfiun3 5992 . . . . . . . . . . . . . . 15 𝑥𝑧 (𝑥𝐴) = ran (𝑥𝑧 ↦ (𝑥𝐴))
2725, 26eqtr4di 2798 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = 𝑥𝑧 (𝑥𝐴))
28 iunin1 5095 . . . . . . . . . . . . . 14 𝑥𝑧 (𝑥𝐴) = ( 𝑥𝑧 𝑥𝐴)
2927, 28eqtrdi 2796 . . . . . . . . . . . . 13 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ( 𝑥𝑧 𝑥𝐴))
30 fvex 6933 . . . . . . . . . . . . . 14 (topGen‘𝐵) ∈ V
31 simpr 484 . . . . . . . . . . . . . 14 ((𝐵𝑉𝐴𝑊) → 𝐴𝑊)
32 uniiun 5081 . . . . . . . . . . . . . . . 16 𝑧 = 𝑥𝑧 𝑥
33 eltg3i 22989 . . . . . . . . . . . . . . . 16 ((𝐵𝑉𝑧𝐵) → 𝑧 ∈ (topGen‘𝐵))
3432, 33eqeltrrid 2849 . . . . . . . . . . . . . . 15 ((𝐵𝑉𝑧𝐵) → 𝑥𝑧 𝑥 ∈ (topGen‘𝐵))
3534adantlr 714 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝑥𝑧 𝑥 ∈ (topGen‘𝐵))
36 elrestr 17488 . . . . . . . . . . . . . 14 (((topGen‘𝐵) ∈ V ∧ 𝐴𝑊 𝑥𝑧 𝑥 ∈ (topGen‘𝐵)) → ( 𝑥𝑧 𝑥𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴))
3730, 31, 35, 36mp3an2ani 1468 . . . . . . . . . . . . 13 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ( 𝑥𝑧 𝑥𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴))
3829, 37eqeltrd 2844 . . . . . . . . . . . 12 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴))
39 unieq 4942 . . . . . . . . . . . . 13 (𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) → 𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧))
4039eleq1d 2829 . . . . . . . . . . . 12 (𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) → ( 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴)))
4138, 40syl5ibrcom 247 . . . . . . . . . . 11 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4241expimpd 453 . . . . . . . . . 10 ((𝐵𝑉𝐴𝑊) → ((𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4342exlimdv 1932 . . . . . . . . 9 ((𝐵𝑉𝐴𝑊) → (∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4443adantr 480 . . . . . . . 8 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → (∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4519, 44mpd 15 . . . . . . 7 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))
46 eleq1 2832 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4745, 46syl5ibrcom 247 . . . . . 6 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → (𝑥 = 𝑦𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4847expimpd 453 . . . . 5 ((𝐵𝑉𝐴𝑊) → ((𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4948exlimdv 1932 . . . 4 ((𝐵𝑉𝐴𝑊) → (∃𝑦(𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
503, 49biimtrid 242 . . 3 ((𝐵𝑉𝐴𝑊) → (𝑥 ∈ (topGen‘(𝐵t 𝐴)) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
5150ssrdv 4014 . 2 ((𝐵𝑉𝐴𝑊) → (topGen‘(𝐵t 𝐴)) ⊆ ((topGen‘𝐵) ↾t 𝐴))
52 restval 17486 . . . 4 (((topGen‘𝐵) ∈ V ∧ 𝐴𝑊) → ((topGen‘𝐵) ↾t 𝐴) = ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)))
5330, 31, 52sylancr 586 . . 3 ((𝐵𝑉𝐴𝑊) → ((topGen‘𝐵) ↾t 𝐴) = ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)))
54 eltg3 22990 . . . . . . . 8 (𝐵𝑉 → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧𝐵𝑤 = 𝑧)))
5554adantr 480 . . . . . . 7 ((𝐵𝑉𝐴𝑊) → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧𝐵𝑤 = 𝑧)))
5632ineq1i 4237 . . . . . . . . . . . 12 ( 𝑧𝐴) = ( 𝑥𝑧 𝑥𝐴)
5756, 28eqtr4i 2771 . . . . . . . . . . 11 ( 𝑧𝐴) = 𝑥𝑧 (𝑥𝐴)
58 simplll 774 . . . . . . . . . . . . . . . 16 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → 𝐵𝑉)
59 simpllr 775 . . . . . . . . . . . . . . . 16 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → 𝐴𝑊)
60 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝑧𝐵)
6160sselda 4008 . . . . . . . . . . . . . . . 16 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → 𝑥𝐵)
62 elrestr 17488 . . . . . . . . . . . . . . . 16 ((𝐵𝑉𝐴𝑊𝑥𝐵) → (𝑥𝐴) ∈ (𝐵t 𝐴))
6358, 59, 61, 62syl3anc 1371 . . . . . . . . . . . . . . 15 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → (𝑥𝐴) ∈ (𝐵t 𝐴))
6463fmpttd 7149 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (𝑥𝑧 ↦ (𝑥𝐴)):𝑧⟶(𝐵t 𝐴))
6564frnd 6755 . . . . . . . . . . . . 13 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ⊆ (𝐵t 𝐴))
66 eltg3i 22989 . . . . . . . . . . . . 13 (((𝐵t 𝐴) ∈ V ∧ ran (𝑥𝑧 ↦ (𝑥𝐴)) ⊆ (𝐵t 𝐴)) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ∈ (topGen‘(𝐵t 𝐴)))
671, 65, 66sylancr 586 . . . . . . . . . . . 12 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ∈ (topGen‘(𝐵t 𝐴)))
6826, 67eqeltrid 2848 . . . . . . . . . . 11 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝑥𝑧 (𝑥𝐴) ∈ (topGen‘(𝐵t 𝐴)))
6957, 68eqeltrid 2848 . . . . . . . . . 10 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ( 𝑧𝐴) ∈ (topGen‘(𝐵t 𝐴)))
70 ineq1 4234 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑤𝐴) = ( 𝑧𝐴))
7170eleq1d 2829 . . . . . . . . . 10 (𝑤 = 𝑧 → ((𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴)) ↔ ( 𝑧𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7269, 71syl5ibrcom 247 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (𝑤 = 𝑧 → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7372expimpd 453 . . . . . . . 8 ((𝐵𝑉𝐴𝑊) → ((𝑧𝐵𝑤 = 𝑧) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7473exlimdv 1932 . . . . . . 7 ((𝐵𝑉𝐴𝑊) → (∃𝑧(𝑧𝐵𝑤 = 𝑧) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7555, 74sylbid 240 . . . . . 6 ((𝐵𝑉𝐴𝑊) → (𝑤 ∈ (topGen‘𝐵) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7675imp 406 . . . . 5 (((𝐵𝑉𝐴𝑊) ∧ 𝑤 ∈ (topGen‘𝐵)) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴)))
7776fmpttd 7149 . . . 4 ((𝐵𝑉𝐴𝑊) → (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)):(topGen‘𝐵)⟶(topGen‘(𝐵t 𝐴)))
7877frnd 6755 . . 3 ((𝐵𝑉𝐴𝑊) → ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)) ⊆ (topGen‘(𝐵t 𝐴)))
7953, 78eqsstrd 4047 . 2 ((𝐵𝑉𝐴𝑊) → ((topGen‘𝐵) ↾t 𝐴) ⊆ (topGen‘(𝐵t 𝐴)))
8051, 79eqssd 4026 1 ((𝐵𝑉𝐴𝑊) → (topGen‘(𝐵t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wex 1777  wcel 2108  wral 3067  Vcvv 3488  cin 3975  wss 3976   cuni 4931   ciun 5015  cmpt 5249  ran crn 5701  cres 5702  cima 5703  Fun wfun 6567   Fn wfn 6568  cfv 6573  (class class class)co 7448  t crest 17480  topGenctg 17497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-rest 17482  df-topgen 17503
This theorem is referenced by:  resttop  23189  ordtrest2  23233  2ndcrest  23483  txrest  23660  xkoptsub  23683  xrtgioo  24847  ordtrest2NEW  33869  ptrest  37579
  Copyright terms: Public domain W3C validator