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

Theorem tgqtop 22327
 Description: An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypothesis
Ref Expression
qtopcmp.1 𝑋 = 𝐽
Assertion
Ref Expression
tgqtop ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹)))

Proof of Theorem tgqtop
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1ocnv 6603 . . . . . . . . 9 (𝐹:𝑋1-1-onto𝑌𝐹:𝑌1-1-onto𝑋)
2 f1ofun 6593 . . . . . . . . 9 (𝐹:𝑌1-1-onto𝑋 → Fun 𝐹)
31, 2syl 17 . . . . . . . 8 (𝐹:𝑋1-1-onto𝑌 → Fun 𝐹)
43ad2antlr 726 . . . . . . 7 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → Fun 𝐹)
5 simpr 488 . . . . . . . 8 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → 𝑥𝑌)
6 df-rn 5531 . . . . . . . . 9 ran 𝐹 = dom 𝐹
7 f1ofo 6598 . . . . . . . . . . 11 (𝐹:𝑋1-1-onto𝑌𝐹:𝑋onto𝑌)
87ad2antlr 726 . . . . . . . . . 10 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → 𝐹:𝑋onto𝑌)
9 forn 6569 . . . . . . . . . 10 (𝐹:𝑋onto𝑌 → ran 𝐹 = 𝑌)
108, 9syl 17 . . . . . . . . 9 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → ran 𝐹 = 𝑌)
116, 10syl5eqr 2847 . . . . . . . 8 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → dom 𝐹 = 𝑌)
125, 11sseqtrrd 3956 . . . . . . 7 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → 𝑥 ⊆ dom 𝐹)
13 funimass4 6706 . . . . . . 7 ((Fun 𝐹𝑥 ⊆ dom 𝐹) → ((𝐹𝑥) ⊆ (𝐽 ∩ 𝒫 (𝐹𝑥)) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))))
144, 12, 13syl2anc 587 . . . . . 6 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → ((𝐹𝑥) ⊆ (𝐽 ∩ 𝒫 (𝐹𝑥)) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))))
15 dfss3 3903 . . . . . . 7 (𝑥 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦𝑥 𝑦 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))
16 simprl 770 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))
1716elin1d 4125 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑧 ∈ (𝐽 qTop 𝐹))
18 qtopcmp.1 . . . . . . . . . . . . . . . . . 18 𝑋 = 𝐽
1918elqtop2 22316 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋onto𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧𝑌 ∧ (𝐹𝑧) ∈ 𝐽)))
207, 19sylan2 595 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧𝑌 ∧ (𝐹𝑧) ∈ 𝐽)))
2120ad3antrrr 729 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧𝑌 ∧ (𝐹𝑧) ∈ 𝐽)))
2217, 21mpbid 235 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝑧𝑌 ∧ (𝐹𝑧) ∈ 𝐽))
2322simprd 499 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝐹𝑧) ∈ 𝐽)
2416elin2d 4126 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑧 ∈ 𝒫 𝑥)
2524elpwid 4508 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑧𝑥)
26 imass2 5933 . . . . . . . . . . . . . . 15 (𝑧𝑥 → (𝐹𝑧) ⊆ (𝐹𝑥))
2725, 26syl 17 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝐹𝑧) ⊆ (𝐹𝑥))
2823, 27elpwd 4505 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝐹𝑧) ∈ 𝒫 (𝐹𝑥))
2923, 28elind 4121 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝐹𝑧) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)))
30 simp-4r 783 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝐹:𝑋1-1-onto𝑌)
3130, 1syl 17 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝐹:𝑌1-1-onto𝑋)
32 f1ofn 6592 . . . . . . . . . . . . . 14 (𝐹:𝑌1-1-onto𝑋𝐹 Fn 𝑌)
3331, 32syl 17 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝐹 Fn 𝑌)
345ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑥𝑌)
3525, 34sstrd 3925 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑧𝑌)
36 simprr 772 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → 𝑦𝑧)
37 fnfvima 6974 . . . . . . . . . . . . 13 ((𝐹 Fn 𝑌𝑧𝑌𝑦𝑧) → (𝐹𝑦) ∈ (𝐹𝑧))
3833, 35, 36, 37syl3anc 1368 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → (𝐹𝑦) ∈ (𝐹𝑧))
39 eleq2 2878 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑧) → ((𝐹𝑦) ∈ 𝑤 ↔ (𝐹𝑦) ∈ (𝐹𝑧)))
4039rspcev 3571 . . . . . . . . . . . 12 (((𝐹𝑧) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ (𝐹𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))(𝐹𝑦) ∈ 𝑤)
4129, 38, 40syl2anc 587 . . . . . . . . . . 11 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))(𝐹𝑦) ∈ 𝑤)
4241rexlimdvaa 3244 . . . . . . . . . 10 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦𝑧 → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))(𝐹𝑦) ∈ 𝑤))
43 simp-4r 783 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝐹:𝑋1-1-onto𝑌)
44 f1ofun 6593 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋1-1-onto𝑌 → Fun 𝐹)
4543, 44syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → Fun 𝐹)
46 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)))
4746elin2d 4126 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝒫 (𝐹𝑥))
4847elpwid 4508 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑤 ⊆ (𝐹𝑥))
49 funimass2 6408 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑤 ⊆ (𝐹𝑥)) → (𝐹𝑤) ⊆ 𝑥)
5045, 48, 49syl2anc 587 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹𝑤) ⊆ 𝑥)
515ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑥𝑌)
5250, 51sstrd 3925 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹𝑤) ⊆ 𝑌)
53 f1of1 6590 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋1-1-onto𝑌𝐹:𝑋1-1𝑌)
5443, 53syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝐹:𝑋1-1𝑌)
5546elin1d 4125 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑤𝐽)
56 elssuni 4831 . . . . . . . . . . . . . . . . . 18 (𝑤𝐽𝑤 𝐽)
5756, 18sseqtrrdi 3966 . . . . . . . . . . . . . . . . 17 (𝑤𝐽𝑤𝑋)
5855, 57syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑤𝑋)
59 f1imacnv 6607 . . . . . . . . . . . . . . . 16 ((𝐹:𝑋1-1𝑌𝑤𝑋) → (𝐹 “ (𝐹𝑤)) = 𝑤)
6054, 58, 59syl2anc 587 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹 “ (𝐹𝑤)) = 𝑤)
6160, 55eqeltrd 2890 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹 “ (𝐹𝑤)) ∈ 𝐽)
6218elqtop2 22316 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋onto𝑌) → ((𝐹𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹𝑤) ⊆ 𝑌 ∧ (𝐹 “ (𝐹𝑤)) ∈ 𝐽)))
637, 62sylan2 595 . . . . . . . . . . . . . . 15 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → ((𝐹𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹𝑤) ⊆ 𝑌 ∧ (𝐹 “ (𝐹𝑤)) ∈ 𝐽)))
6463ad3antrrr 729 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → ((𝐹𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹𝑤) ⊆ 𝑌 ∧ (𝐹 “ (𝐹𝑤)) ∈ 𝐽)))
6552, 61, 64mpbir2and 712 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹𝑤) ∈ (𝐽 qTop 𝐹))
66 vex 3444 . . . . . . . . . . . . . . 15 𝑥 ∈ V
6766elpw2 5213 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ 𝒫 𝑥 ↔ (𝐹𝑤) ⊆ 𝑥)
6850, 67sylibr 237 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹𝑤) ∈ 𝒫 𝑥)
6965, 68elind 4121 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))
705sselda 3915 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → 𝑦𝑌)
7170adantr 484 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑦𝑌)
72 f1ocnvfv2 7013 . . . . . . . . . . . . . 14 ((𝐹:𝑋1-1-onto𝑌𝑦𝑌) → (𝐹‘(𝐹𝑦)) = 𝑦)
7343, 71, 72syl2anc 587 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹‘(𝐹𝑦)) = 𝑦)
74 f1ofn 6592 . . . . . . . . . . . . . . . 16 (𝐹:𝑋1-1-onto𝑌𝐹 Fn 𝑋)
7574adantl 485 . . . . . . . . . . . . . . 15 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → 𝐹 Fn 𝑋)
7675ad3antrrr 729 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝐹 Fn 𝑋)
77 simprr 772 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹𝑦) ∈ 𝑤)
78 fnfvima 6974 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋𝑤𝑋 ∧ (𝐹𝑦) ∈ 𝑤) → (𝐹‘(𝐹𝑦)) ∈ (𝐹𝑤))
7976, 58, 77, 78syl3anc 1368 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → (𝐹‘(𝐹𝑦)) ∈ (𝐹𝑤))
8073, 79eqeltrrd 2891 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → 𝑦 ∈ (𝐹𝑤))
81 eleq2 2878 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑤) → (𝑦𝑧𝑦 ∈ (𝐹𝑤)))
8281rspcev 3571 . . . . . . . . . . . 12 (((𝐹𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ (𝐹𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦𝑧)
8369, 80, 82syl2anc 587 . . . . . . . . . . 11 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ∧ (𝐹𝑦) ∈ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦𝑧)
8483rexlimdvaa 3244 . . . . . . . . . 10 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))(𝐹𝑦) ∈ 𝑤 → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦𝑧))
8542, 84impbid 215 . . . . . . . . 9 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦𝑧 ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))(𝐹𝑦) ∈ 𝑤))
86 eluni2 4805 . . . . . . . . 9 (𝑦 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦𝑧)
87 eluni2 4805 . . . . . . . . 9 ((𝐹𝑦) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥)) ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))(𝐹𝑦) ∈ 𝑤)
8885, 86, 873bitr4g 317 . . . . . . . 8 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (𝑦 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ (𝐹𝑦) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))))
8988ralbidva 3161 . . . . . . 7 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → (∀𝑦𝑥 𝑦 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))))
9015, 89syl5bb 286 . . . . . 6 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → (𝑥 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐽 ∩ 𝒫 (𝐹𝑥))))
9114, 90bitr4d 285 . . . . 5 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → ((𝐹𝑥) ⊆ (𝐽 ∩ 𝒫 (𝐹𝑥)) ↔ 𝑥 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)))
92 eltg 21572 . . . . . 6 (𝐽 ∈ TopBases → ((𝐹𝑥) ∈ (topGen‘𝐽) ↔ (𝐹𝑥) ⊆ (𝐽 ∩ 𝒫 (𝐹𝑥))))
9392ad2antrr 725 . . . . 5 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → ((𝐹𝑥) ∈ (topGen‘𝐽) ↔ (𝐹𝑥) ⊆ (𝐽 ∩ 𝒫 (𝐹𝑥))))
94 ovex 7169 . . . . . 6 (𝐽 qTop 𝐹) ∈ V
95 eltg 21572 . . . . . 6 ((𝐽 qTop 𝐹) ∈ V → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)))
9694, 95mp1i 13 . . . . 5 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)))
9791, 93, 963bitr4d 314 . . . 4 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) ∧ 𝑥𝑌) → ((𝐹𝑥) ∈ (topGen‘𝐽) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))
9897pm5.32da 582 . . 3 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → ((𝑥𝑌 ∧ (𝐹𝑥) ∈ (topGen‘𝐽)) ↔ (𝑥𝑌𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))))
99 tgtopon 21586 . . . . . 6 (𝐽 ∈ TopBases → (topGen‘𝐽) ∈ (TopOn‘ 𝐽))
10099adantr 484 . . . . 5 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (topGen‘𝐽) ∈ (TopOn‘ 𝐽))
10118fveq2i 6649 . . . . 5 (TopOn‘𝑋) = (TopOn‘ 𝐽)
102100, 101eleqtrrdi 2901 . . . 4 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (topGen‘𝐽) ∈ (TopOn‘𝑋))
1037adantl 485 . . . 4 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → 𝐹:𝑋onto𝑌)
104 elqtop3 22318 . . . 4 (((topGen‘𝐽) ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ (topGen‘𝐽))))
105102, 103, 104syl2anc 587 . . 3 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ (topGen‘𝐽))))
106 unitg 21582 . . . . . . . . 9 ((𝐽 qTop 𝐹) ∈ V → (topGen‘(𝐽 qTop 𝐹)) = (𝐽 qTop 𝐹))
10794, 106ax-mp 5 . . . . . . . 8 (topGen‘(𝐽 qTop 𝐹)) = (𝐽 qTop 𝐹)
10818elqtop2 22316 . . . . . . . . . . . 12 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
1097, 108sylan2 595 . . . . . . . . . . 11 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
110 simpl 486 . . . . . . . . . . . 12 ((𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽) → 𝑥𝑌)
111 velpw 4502 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝑌𝑥𝑌)
112110, 111sylibr 237 . . . . . . . . . . 11 ((𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽) → 𝑥 ∈ 𝒫 𝑌)
113109, 112syl6bi 256 . . . . . . . . . 10 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) → 𝑥 ∈ 𝒫 𝑌))
114113ssrdv 3921 . . . . . . . . 9 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝐽 qTop 𝐹) ⊆ 𝒫 𝑌)
115 sspwuni 4986 . . . . . . . . 9 ((𝐽 qTop 𝐹) ⊆ 𝒫 𝑌 (𝐽 qTop 𝐹) ⊆ 𝑌)
116114, 115sylib 221 . . . . . . . 8 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝐽 qTop 𝐹) ⊆ 𝑌)
117107, 116eqsstrid 3963 . . . . . . 7 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌)
118 sspwuni 4986 . . . . . . 7 ((topGen‘(𝐽 qTop 𝐹)) ⊆ 𝒫 𝑌 (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌)
119117, 118sylibr 237 . . . . . 6 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝒫 𝑌)
120119sseld 3914 . . . . 5 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ∈ 𝒫 𝑌))
121120, 111syl6ib 254 . . . 4 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥𝑌))
122121pm4.71rd 566 . . 3 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ (𝑥𝑌𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))))
12398, 105, 1223bitr4d 314 . 2 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))
124123eqrdv 2796 1 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋1-1-onto𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497  ∪ cuni 4801  ◡ccnv 5519  dom cdm 5520  ran crn 5521   “ cima 5523  Fun wfun 6319   Fn wfn 6320  –1-1→wf1 6322  –onto→wfo 6323  –1-1-onto→wf1o 6324  ‘cfv 6325  (class class class)co 7136  topGenctg 16706   qTop cqtop 16771  TopOnctopon 21525  TopBasesctb 21560 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-ov 7139  df-oprab 7140  df-mpo 7141  df-topgen 16712  df-qtop 16775  df-top 21509  df-topon 21526  df-bases 21561 This theorem is referenced by:  imasf1oxms  23106
 Copyright terms: Public domain W3C validator