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

Theorem alexsubALT 23308
Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
alexsubALT.1 𝑋 = 𝐽
Assertion
Ref Expression
alexsubALT (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
Distinct variable groups:   𝑐,𝑑,𝑥,𝐽   𝑋,𝑐,𝑑,𝑥

Proof of Theorem alexsubALT
Dummy variables 𝑎 𝑏 𝑓 𝑡 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 alexsubALT.1 . . 3 𝑋 = 𝐽
21alexsubALTlem1 23304 . 2 (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
31alexsubALTlem4 23307 . . . . 5 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
4 velpw 4552 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
5 eleq2 2825 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑐 → (𝑡𝑋𝑡 𝑐))
653ad2ant3 1134 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋𝑡 𝑐))
7 eluni 4855 . . . . . . . . . . . . . . . . . . . 20 (𝑡 𝑐 ↔ ∃𝑤(𝑡𝑤𝑤𝑐))
8 ssel 3925 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐𝐽 → (𝑤𝑐𝑤𝐽))
9 eleq2 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤𝐽𝑤 ∈ (topGen‘(fi‘𝑥))))
10 tg2 22221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤 ∈ (topGen‘(fi‘𝑥)) ∧ 𝑡𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤))
1110ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (topGen‘(fi‘𝑥)) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤)))
129, 11syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤𝐽 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤))))
138, 12sylan9r 509 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑤𝑐 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤))))
14133impia 1116 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤)))
15 sseq2 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑤 → (𝑦𝑧𝑦𝑤))
1615rspcev 3570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤𝑐𝑦𝑤) → ∃𝑧𝑐 𝑦𝑧)
1716ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑐 → (𝑦𝑤 → ∃𝑧𝑐 𝑦𝑧))
18173ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑦𝑤 → ∃𝑧𝑐 𝑦𝑧))
1918anim2d 612 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → ((𝑡𝑦𝑦𝑤) → (𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2019reximdv 3163 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2114, 20syld 47 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
22213expia 1120 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑤𝑐 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))))
2322com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑡𝑤 → (𝑤𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))))
2423impd 411 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → ((𝑡𝑤𝑤𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2524exlimdv 1935 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (∃𝑤(𝑡𝑤𝑤𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
267, 25biimtrid 241 . . . . . . . . . . . . . . . . . . 19 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑡 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
27263adant3 1131 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
286, 27sylbid 239 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
29 ssel 3925 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑧 → (𝑡𝑦𝑡𝑧))
30 elunii 4857 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡𝑧𝑧𝑐) → 𝑡 𝑐)
3130expcom 414 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑐 → (𝑡𝑧𝑡 𝑐))
326biimprd 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡 𝑐𝑡𝑋))
3331, 32sylan9r 509 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑧𝑐) → (𝑡𝑧𝑡𝑋))
3429, 33syl9r 78 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑧𝑐) → (𝑦𝑧 → (𝑡𝑦𝑡𝑋)))
3534rexlimdva 3148 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑧𝑐 𝑦𝑧 → (𝑡𝑦𝑡𝑋)))
3635com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑦 → (∃𝑧𝑐 𝑦𝑧𝑡𝑋)))
3736impd 411 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → ((𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧) → 𝑡𝑋))
3837rexlimdvw 3153 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧) → 𝑡𝑋))
3928, 38impbid 211 . . . . . . . . . . . . . . . 16 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
40 elunirab 4868 . . . . . . . . . . . . . . . 16 (𝑡 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))
4139, 40bitr4di 288 . . . . . . . . . . . . . . 15 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋𝑡 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
4241eqrdv 2734 . . . . . . . . . . . . . 14 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → 𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
43 ssrab2 4025 . . . . . . . . . . . . . . . 16 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ⊆ (fi‘𝑥)
44 fvex 6838 . . . . . . . . . . . . . . . . 17 (fi‘𝑥) ∈ V
4544elpw2 5289 . . . . . . . . . . . . . . . 16 ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ⊆ (fi‘𝑥))
4643, 45mpbir 230 . . . . . . . . . . . . . . 15 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥)
47 unieq 4863 . . . . . . . . . . . . . . . . . 18 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → 𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
4847eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑎𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
49 pweq 4561 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
5049ineq1d 4158 . . . . . . . . . . . . . . . . . 18 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin))
5150rexeqdv 3310 . . . . . . . . . . . . . . . . 17 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏))
5248, 51imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ((𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ (𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏)))
5352rspcv 3566 . . . . . . . . . . . . . . 15 ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏)))
5446, 53ax-mp 5 . . . . . . . . . . . . . 14 (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏))
5542, 54syl5com 31 . . . . . . . . . . . . 13 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏))
56 elfpw 9219 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∧ 𝑏 ∈ Fin))
57 ssel 3925 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑡𝑏𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
58 sseq1 3957 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑡 → (𝑦𝑧𝑡𝑧))
5958rexbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑡 → (∃𝑧𝑐 𝑦𝑧 ↔ ∃𝑧𝑐 𝑡𝑧))
6059elrab 3634 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧𝑐 𝑡𝑧))
6160simprbi 497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑧𝑐 𝑡𝑧)
6257, 61syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑡𝑏 → ∃𝑧𝑐 𝑡𝑧))
6362ralrimiv 3138 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∀𝑡𝑏𝑧𝑐 𝑡𝑧)
64 sseq2 3958 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑓𝑡) → (𝑡𝑧𝑡 ⊆ (𝑓𝑡)))
6564ac6sfi 9152 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ Fin ∧ ∀𝑡𝑏𝑧𝑐 𝑡𝑧) → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)))
6665ex 413 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ Fin → (∀𝑡𝑏𝑧𝑐 𝑡𝑧 → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
6763, 66syl5 34 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
6867adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
69 simprll 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑓:𝑏𝑐)
70 frn 6658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑏𝑐 → ran 𝑓𝑐)
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑐)
72 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 ∈ Fin)
73 ffn 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:𝑏𝑐𝑓 Fn 𝑏)
74 dffn4 6745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn 𝑏𝑓:𝑏onto→ran 𝑓)
7573, 74sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑏𝑐𝑓:𝑏onto→ran 𝑓)
7675adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → 𝑓:𝑏onto→ran 𝑓)
7776ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑓:𝑏onto→ran 𝑓)
78 fodomfi 9190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏 ∈ Fin ∧ 𝑓:𝑏onto→ran 𝑓) → ran 𝑓𝑏)
7972, 77, 78syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑏)
80 domfi 9057 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∈ Fin ∧ ran 𝑓𝑏) → ran 𝑓 ∈ Fin)
8172, 79, 80syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓 ∈ Fin)
8271, 81jca 512 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → (ran 𝑓𝑐 ∧ ran 𝑓 ∈ Fin))
83 elin 3914 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84 vex 3445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑐 ∈ V
8584elpw2 5289 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
8685anbi1i 624 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ (ran 𝑓𝑐 ∧ ran 𝑓 ∈ Fin))
8783, 86bitr2i 275 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑓𝑐 ∧ ran 𝑓 ∈ Fin) ↔ ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
8882, 87sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
89 simprr 770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 = 𝑏)
90 uniiun 5005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑡𝑏 𝑡
91 simprlr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))
92 ss2iun 4959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡) → 𝑡𝑏 𝑡 𝑡𝑏 (𝑓𝑡))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑡𝑏 𝑡 𝑡𝑏 (𝑓𝑡))
9490, 93eqsstrid 3980 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 𝑡𝑏 (𝑓𝑡))
95 fniunfv 7176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑏 𝑡𝑏 (𝑓𝑡) = ran 𝑓)
9669, 73, 953syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑡𝑏 (𝑓𝑡) = ran 𝑓)
9794, 96sseqtrd 3972 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 ran 𝑓)
9889, 97eqsstrd 3970 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 ran 𝑓)
99 simpll2 1212 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑐𝐽)
10071, 99sstrd 3942 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝐽)
101 uniss 4860 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑓𝐽 ran 𝑓 𝐽)
102101, 1sseqtrrdi 3983 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑓𝐽 ran 𝑓𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑋)
10498, 103eqssd 3949 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 = ran 𝑓)
105 unieq 4863 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
106105eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = ran 𝑓 → (𝑋 = 𝑑𝑋 = ran 𝑓))
107106rspcev 3570 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
10888, 104, 107syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
109108exp32 421 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
110109exlimdv 1935 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
11168, 110syld 47 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
112111ex 413 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
113112com23 86 . . . . . . . . . . . . . . . 16 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑏 ∈ Fin → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
114113impd 411 . . . . . . . . . . . . . . 15 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → ((𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∧ 𝑏 ∈ Fin) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
11556, 114biimtrid 241 . . . . . . . . . . . . . 14 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
116115rexlimdv 3146 . . . . . . . . . . . . 13 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
11755, 116syld 47 . . . . . . . . . . . 12 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
1181173exp 1118 . . . . . . . . . . 11 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐𝐽 → (𝑋 = 𝑐 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
119118com34 91 . . . . . . . . . 10 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐𝐽 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
120119com23 86 . . . . . . . . 9 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑐𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
1214, 120syl7bi 254 . . . . . . . 8 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
122121ralrimdv 3145 . . . . . . 7 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
123 fibas 22233 . . . . . . . . 9 (fi‘𝑥) ∈ TopBases
124 tgcl 22225 . . . . . . . . 9 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125123, 124ax-mp 5 . . . . . . . 8 (topGen‘(fi‘𝑥)) ∈ Top
126 eleq1 2824 . . . . . . . 8 (𝐽 = (topGen‘(fi‘𝑥)) → (𝐽 ∈ Top ↔ (topGen‘(fi‘𝑥)) ∈ Top))
127125, 126mpbiri 257 . . . . . . 7 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 ∈ Top)
128122, 127jctild 526 . . . . . 6 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
1291iscmp 22645 . . . . . 6 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
130128, 129syl6ibr 251 . . . . 5 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → 𝐽 ∈ Comp))
1313, 130syld 47 . . . 4 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → 𝐽 ∈ Comp))
132131imp 407 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)) → 𝐽 ∈ Comp)
133132exlimiv 1932 . 2 (∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)) → 𝐽 ∈ Comp)
1342, 133impbii 208 1 (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wral 3061  wrex 3070  {crab 3403  cin 3897  wss 3898  𝒫 cpw 4547   cuni 4852   ciun 4941   class class class wbr 5092  ran crn 5621   Fn wfn 6474  wf 6475  ontowfo 6477  cfv 6479  cdom 8802  Fincfn 8804  ficfi 9267  topGenctg 17245  Topctop 22148  TopBasesctb 22201  Compccmp 22643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-ac2 10320
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-rpss 7638  df-om 7781  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-1o 8367  df-er 8569  df-en 8805  df-dom 8806  df-fin 8808  df-fi 9268  df-card 9796  df-ac 9973  df-topgen 17251  df-top 22149  df-bases 22202  df-cmp 22644
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator