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

Theorem tgrest 20868
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 6633 . . . . 5 (𝐵t 𝐴) ∈ V
2 eltg3 20672 . . . . 5 ((𝐵t 𝐴) ∈ V → (𝑥 ∈ (topGen‘(𝐵t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦)))
31, 2ax-mp 5 . . . 4 (𝑥 ∈ (topGen‘(𝐵t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦))
4 simpll 789 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝐵𝑉)
5 funmpt 5886 . . . . . . . . . 10 Fun (𝑥𝐵 ↦ (𝑥𝐴))
65a1i 11 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → Fun (𝑥𝐵 ↦ (𝑥𝐴)))
7 restval 16003 . . . . . . . . . . . 12 ((𝐵𝑉𝐴𝑊) → (𝐵t 𝐴) = ran (𝑥𝐵 ↦ (𝑥𝐴)))
87sseq2d 3617 . . . . . . . . . . 11 ((𝐵𝑉𝐴𝑊) → (𝑦 ⊆ (𝐵t 𝐴) ↔ 𝑦 ⊆ ran (𝑥𝐵 ↦ (𝑥𝐴))))
98biimpa 501 . . . . . . . . . 10 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝑦 ⊆ ran (𝑥𝐵 ↦ (𝑥𝐴)))
10 vex 3194 . . . . . . . . . . . . 13 𝑥 ∈ V
1110inex1 4764 . . . . . . . . . . . 12 (𝑥𝐴) ∈ V
1211rgenw 2924 . . . . . . . . . . 11 𝑥𝐵 (𝑥𝐴) ∈ V
13 eqid 2626 . . . . . . . . . . . 12 (𝑥𝐵 ↦ (𝑥𝐴)) = (𝑥𝐵 ↦ (𝑥𝐴))
1413fnmpt 5979 . . . . . . . . . . 11 (∀𝑥𝐵 (𝑥𝐴) ∈ V → (𝑥𝐵 ↦ (𝑥𝐴)) Fn 𝐵)
15 fnima 5969 . . . . . . . . . . 11 ((𝑥𝐵 ↦ (𝑥𝐴)) Fn 𝐵 → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵) = ran (𝑥𝐵 ↦ (𝑥𝐴)))
1612, 14, 15mp2b 10 . . . . . . . . . 10 ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵) = ran (𝑥𝐵 ↦ (𝑥𝐴))
179, 16syl6sseqr 3636 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝑦 ⊆ ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵))
18 ssimaexg 6222 . . . . . . . . 9 ((𝐵𝑉 ∧ Fun (𝑥𝐵 ↦ (𝑥𝐴)) ∧ 𝑦 ⊆ ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝐵)) → ∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)))
194, 6, 17, 18syl3anc 1323 . . . . . . . 8 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → ∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)))
20 df-ima 5092 . . . . . . . . . . . . . . . . 17 ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ran ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧)
21 resmpt 5412 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐵 → ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧) = (𝑥𝑧 ↦ (𝑥𝐴)))
2221adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧) = (𝑥𝑧 ↦ (𝑥𝐴)))
2322rneqd 5317 . . . . . . . . . . . . . . . . 17 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ran ((𝑥𝐵 ↦ (𝑥𝐴)) ↾ 𝑧) = ran (𝑥𝑧 ↦ (𝑥𝐴)))
2420, 23syl5eq 2672 . . . . . . . . . . . . . . . 16 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ran (𝑥𝑧 ↦ (𝑥𝐴)))
2524unieqd 4417 . . . . . . . . . . . . . . 15 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ran (𝑥𝑧 ↦ (𝑥𝐴)))
2611dfiun3 5344 . . . . . . . . . . . . . . 15 𝑥𝑧 (𝑥𝐴) = ran (𝑥𝑧 ↦ (𝑥𝐴))
2725, 26syl6eqr 2678 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = 𝑥𝑧 (𝑥𝐴))
28 iunin1 4556 . . . . . . . . . . . . . 14 𝑥𝑧 (𝑥𝐴) = ( 𝑥𝑧 𝑥𝐴)
2927, 28syl6eq 2676 . . . . . . . . . . . . 13 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) = ( 𝑥𝑧 𝑥𝐴))
30 fvex 6160 . . . . . . . . . . . . . . 15 (topGen‘𝐵) ∈ V
3130a1i 11 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (topGen‘𝐵) ∈ V)
32 simpr 477 . . . . . . . . . . . . . . 15 ((𝐵𝑉𝐴𝑊) → 𝐴𝑊)
3332adantr 481 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝐴𝑊)
34 uniiun 4544 . . . . . . . . . . . . . . . 16 𝑧 = 𝑥𝑧 𝑥
35 eltg3i 20671 . . . . . . . . . . . . . . . 16 ((𝐵𝑉𝑧𝐵) → 𝑧 ∈ (topGen‘𝐵))
3634, 35syl5eqelr 2709 . . . . . . . . . . . . . . 15 ((𝐵𝑉𝑧𝐵) → 𝑥𝑧 𝑥 ∈ (topGen‘𝐵))
3736adantlr 750 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝑥𝑧 𝑥 ∈ (topGen‘𝐵))
38 elrestr 16005 . . . . . . . . . . . . . 14 (((topGen‘𝐵) ∈ V ∧ 𝐴𝑊 𝑥𝑧 𝑥 ∈ (topGen‘𝐵)) → ( 𝑥𝑧 𝑥𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴))
3931, 33, 37, 38syl3anc 1323 . . . . . . . . . . . . 13 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ( 𝑥𝑧 𝑥𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴))
4029, 39eqeltrd 2704 . . . . . . . . . . . 12 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴))
41 unieq 4415 . . . . . . . . . . . . 13 (𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) → 𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧))
4241eleq1d 2688 . . . . . . . . . . . 12 (𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) → ( 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴)))
4340, 42syl5ibrcom 237 . . . . . . . . . . 11 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4443expimpd 628 . . . . . . . . . 10 ((𝐵𝑉𝐴𝑊) → ((𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4544exlimdv 1863 . . . . . . . . 9 ((𝐵𝑉𝐴𝑊) → (∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4645adantr 481 . . . . . . . 8 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → (∃𝑧(𝑧𝐵𝑦 = ((𝑥𝐵 ↦ (𝑥𝐴)) “ 𝑧)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4719, 46mpd 15 . . . . . . 7 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))
48 eleq1 2692 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)))
4947, 48syl5ibrcom 237 . . . . . 6 (((𝐵𝑉𝐴𝑊) ∧ 𝑦 ⊆ (𝐵t 𝐴)) → (𝑥 = 𝑦𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
5049expimpd 628 . . . . 5 ((𝐵𝑉𝐴𝑊) → ((𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
5150exlimdv 1863 . . . 4 ((𝐵𝑉𝐴𝑊) → (∃𝑦(𝑦 ⊆ (𝐵t 𝐴) ∧ 𝑥 = 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
523, 51syl5bi 232 . . 3 ((𝐵𝑉𝐴𝑊) → (𝑥 ∈ (topGen‘(𝐵t 𝐴)) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴)))
5352ssrdv 3594 . 2 ((𝐵𝑉𝐴𝑊) → (topGen‘(𝐵t 𝐴)) ⊆ ((topGen‘𝐵) ↾t 𝐴))
54 restval 16003 . . . 4 (((topGen‘𝐵) ∈ V ∧ 𝐴𝑊) → ((topGen‘𝐵) ↾t 𝐴) = ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)))
5530, 32, 54sylancr 694 . . 3 ((𝐵𝑉𝐴𝑊) → ((topGen‘𝐵) ↾t 𝐴) = ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)))
56 eltg3 20672 . . . . . . . 8 (𝐵𝑉 → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧𝐵𝑤 = 𝑧)))
5756adantr 481 . . . . . . 7 ((𝐵𝑉𝐴𝑊) → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧𝐵𝑤 = 𝑧)))
5834ineq1i 3793 . . . . . . . . . . . 12 ( 𝑧𝐴) = ( 𝑥𝑧 𝑥𝐴)
5958, 28eqtr4i 2651 . . . . . . . . . . 11 ( 𝑧𝐴) = 𝑥𝑧 (𝑥𝐴)
60 simplll 797 . . . . . . . . . . . . . . . 16 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → 𝐵𝑉)
61 simpllr 798 . . . . . . . . . . . . . . . 16 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → 𝐴𝑊)
62 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝑧𝐵)
6362sselda 3588 . . . . . . . . . . . . . . . 16 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → 𝑥𝐵)
64 elrestr 16005 . . . . . . . . . . . . . . . 16 ((𝐵𝑉𝐴𝑊𝑥𝐵) → (𝑥𝐴) ∈ (𝐵t 𝐴))
6560, 61, 63, 64syl3anc 1323 . . . . . . . . . . . . . . 15 ((((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) ∧ 𝑥𝑧) → (𝑥𝐴) ∈ (𝐵t 𝐴))
66 eqid 2626 . . . . . . . . . . . . . . 15 (𝑥𝑧 ↦ (𝑥𝐴)) = (𝑥𝑧 ↦ (𝑥𝐴))
6765, 66fmptd 6341 . . . . . . . . . . . . . 14 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (𝑥𝑧 ↦ (𝑥𝐴)):𝑧⟶(𝐵t 𝐴))
68 frn 6012 . . . . . . . . . . . . . 14 ((𝑥𝑧 ↦ (𝑥𝐴)):𝑧⟶(𝐵t 𝐴) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ⊆ (𝐵t 𝐴))
6967, 68syl 17 . . . . . . . . . . . . 13 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ⊆ (𝐵t 𝐴))
70 eltg3i 20671 . . . . . . . . . . . . 13 (((𝐵t 𝐴) ∈ V ∧ ran (𝑥𝑧 ↦ (𝑥𝐴)) ⊆ (𝐵t 𝐴)) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ∈ (topGen‘(𝐵t 𝐴)))
711, 69, 70sylancr 694 . . . . . . . . . . . 12 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ran (𝑥𝑧 ↦ (𝑥𝐴)) ∈ (topGen‘(𝐵t 𝐴)))
7226, 71syl5eqel 2708 . . . . . . . . . . 11 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → 𝑥𝑧 (𝑥𝐴) ∈ (topGen‘(𝐵t 𝐴)))
7359, 72syl5eqel 2708 . . . . . . . . . 10 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → ( 𝑧𝐴) ∈ (topGen‘(𝐵t 𝐴)))
74 ineq1 3790 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑤𝐴) = ( 𝑧𝐴))
7574eleq1d 2688 . . . . . . . . . 10 (𝑤 = 𝑧 → ((𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴)) ↔ ( 𝑧𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7673, 75syl5ibrcom 237 . . . . . . . . 9 (((𝐵𝑉𝐴𝑊) ∧ 𝑧𝐵) → (𝑤 = 𝑧 → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7776expimpd 628 . . . . . . . 8 ((𝐵𝑉𝐴𝑊) → ((𝑧𝐵𝑤 = 𝑧) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7877exlimdv 1863 . . . . . . 7 ((𝐵𝑉𝐴𝑊) → (∃𝑧(𝑧𝐵𝑤 = 𝑧) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
7957, 78sylbid 230 . . . . . 6 ((𝐵𝑉𝐴𝑊) → (𝑤 ∈ (topGen‘𝐵) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴))))
8079imp 445 . . . . 5 (((𝐵𝑉𝐴𝑊) ∧ 𝑤 ∈ (topGen‘𝐵)) → (𝑤𝐴) ∈ (topGen‘(𝐵t 𝐴)))
81 eqid 2626 . . . . 5 (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)) = (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴))
8280, 81fmptd 6341 . . . 4 ((𝐵𝑉𝐴𝑊) → (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)):(topGen‘𝐵)⟶(topGen‘(𝐵t 𝐴)))
83 frn 6012 . . . 4 ((𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)):(topGen‘𝐵)⟶(topGen‘(𝐵t 𝐴)) → ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)) ⊆ (topGen‘(𝐵t 𝐴)))
8482, 83syl 17 . . 3 ((𝐵𝑉𝐴𝑊) → ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤𝐴)) ⊆ (topGen‘(𝐵t 𝐴)))
8555, 84eqsstrd 3623 . 2 ((𝐵𝑉𝐴𝑊) → ((topGen‘𝐵) ↾t 𝐴) ⊆ (topGen‘(𝐵t 𝐴)))
8653, 85eqssd 3605 1 ((𝐵𝑉𝐴𝑊) → (topGen‘(𝐵t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  wral 2912  Vcvv 3191  cin 3559  wss 3560   cuni 4407   ciun 4490  cmpt 4678  ran crn 5080  cres 5081  cima 5082  Fun wfun 5844   Fn wfn 5845  wf 5846  cfv 5850  (class class class)co 6605  t crest 15997  topGenctg 16014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-rest 15999  df-topgen 16020
This theorem is referenced by:  resttop  20869  ordtrest2  20913  2ndcrest  21162  txrest  21339  xkoptsub  21362  xrtgioo  22512  ordtrest2NEW  29743  ptrest  33026
  Copyright terms: Public domain W3C validator