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

Theorem alexsubALT 23402
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 23398 . 2 (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
31alexsubALTlem4 23401 . . . . 5 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
4 velpw 4565 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
5 eleq2 2826 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑐 → (𝑡𝑋𝑡 𝑐))
653ad2ant3 1135 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋𝑡 𝑐))
7 eluni 4868 . . . . . . . . . . . . . . . . . . . 20 (𝑡 𝑐 ↔ ∃𝑤(𝑡𝑤𝑤𝑐))
8 ssel 3937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐𝐽 → (𝑤𝑐𝑤𝐽))
9 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤𝐽𝑤 ∈ (topGen‘(fi‘𝑥))))
10 tg2 22315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1117 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤)))
15 sseq2 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑤 → (𝑦𝑧𝑦𝑤))
1615rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤𝑐𝑦𝑤) → ∃𝑧𝑐 𝑦𝑧)
1716ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑐 → (𝑦𝑤 → ∃𝑧𝑐 𝑦𝑧))
18173ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑦𝑤 → ∃𝑧𝑐 𝑦𝑧))
1918anim2d 612 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → ((𝑡𝑦𝑦𝑤) → (𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2019reximdv 3167 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2114, 20syld 47 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
22213expia 1121 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑤𝑐 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))))
2322com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑡𝑤 → (𝑤𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))))
2423impd 411 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → ((𝑡𝑤𝑤𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2524exlimdv 1936 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (∃𝑤(𝑡𝑤𝑤𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
267, 25biimtrid 241 . . . . . . . . . . . . . . . . . . 19 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑡 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
27263adant3 1132 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
286, 27sylbid 239 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
29 ssel 3937 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑧 → (𝑡𝑦𝑡𝑧))
30 elunii 4870 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡𝑧𝑧𝑐) → 𝑡 𝑐)
3130expcom 414 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑐 → (𝑡𝑧𝑡 𝑐))
326biimprd 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡 𝑐𝑡𝑋))
3331, 32sylan9r 509 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑧𝑐) → (𝑡𝑧𝑡𝑋))
3429, 33syl9r 78 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑧𝑐) → (𝑦𝑧 → (𝑡𝑦𝑡𝑋)))
3534rexlimdva 3152 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑧𝑐 𝑦𝑧 → (𝑡𝑦𝑡𝑋)))
3635com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑦 → (∃𝑧𝑐 𝑦𝑧𝑡𝑋)))
3736impd 411 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → ((𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧) → 𝑡𝑋))
3837rexlimdvw 3157 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧) → 𝑡𝑋))
3928, 38impbid 211 . . . . . . . . . . . . . . . 16 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
40 elunirab 4881 . . . . . . . . . . . . . . . 16 (𝑡 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))
4139, 40bitr4di 288 . . . . . . . . . . . . . . 15 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋𝑡 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
4241eqrdv 2734 . . . . . . . . . . . . . 14 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → 𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
43 ssrab2 4037 . . . . . . . . . . . . . . . 16 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ⊆ (fi‘𝑥)
44 fvex 6855 . . . . . . . . . . . . . . . . 17 (fi‘𝑥) ∈ V
4544elpw2 5302 . . . . . . . . . . . . . . . 16 ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ⊆ (fi‘𝑥))
4643, 45mpbir 230 . . . . . . . . . . . . . . 15 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥)
47 unieq 4876 . . . . . . . . . . . . . . . . . 18 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → 𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
4847eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑎𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
49 pweq 4574 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
5049ineq1d 4171 . . . . . . . . . . . . . . . . . 18 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin))
5150rexeqdv 3314 . . . . . . . . . . . . . . . . 17 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏))
5248, 51imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ((𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ (𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏)))
5352rspcv 3577 . . . . . . . . . . . . . . 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 9298 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∧ 𝑏 ∈ Fin))
57 ssel 3937 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑡𝑏𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
58 sseq1 3969 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑡 → (𝑦𝑧𝑡𝑧))
5958rexbidv 3175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑡 → (∃𝑧𝑐 𝑦𝑧 ↔ ∃𝑧𝑐 𝑡𝑧))
6059elrab 3645 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧𝑐 𝑡𝑧))
6160simprbi 497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑧𝑐 𝑡𝑧)
6257, 61syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑡𝑏 → ∃𝑧𝑐 𝑡𝑧))
6362ralrimiv 3142 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∀𝑡𝑏𝑧𝑐 𝑡𝑧)
64 sseq2 3970 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑓𝑡) → (𝑡𝑧𝑡 ⊆ (𝑓𝑡)))
6564ac6sfi 9231 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ Fin ∧ ∀𝑡𝑏𝑧𝑐 𝑡𝑧) → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)))
6665ex 413 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ Fin → (∀𝑡𝑏𝑧𝑐 𝑡𝑧 → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
6763, 66syl5 34 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
6867adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
69 simprll 777 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑓:𝑏𝑐)
70 frn 6675 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑏𝑐 → ran 𝑓𝑐)
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑐)
72 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 ∈ Fin)
73 ffn 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:𝑏𝑐𝑓 Fn 𝑏)
74 dffn4 6762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn 𝑏𝑓:𝑏onto→ran 𝑓)
7573, 74sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑏𝑐𝑓:𝑏onto→ran 𝑓)
7675adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → 𝑓:𝑏onto→ran 𝑓)
7776ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑓:𝑏onto→ran 𝑓)
78 fodomfi 9269 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏 ∈ Fin ∧ 𝑓:𝑏onto→ran 𝑓) → ran 𝑓𝑏)
7972, 77, 78syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑏)
80 domfi 9136 . . . . . . . . . . . . . . . . . . . . . . . . 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 3926 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑐 ∈ V
8584elpw2 5302 . . . . . . . . . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 = 𝑏)
90 uniiun 5018 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑡𝑏 𝑡
91 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))
92 ss2iun 4972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡) → 𝑡𝑏 𝑡 𝑡𝑏 (𝑓𝑡))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑡𝑏 𝑡 𝑡𝑏 (𝑓𝑡))
9490, 93eqsstrid 3992 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 𝑡𝑏 (𝑓𝑡))
95 fniunfv 7194 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑏 𝑡𝑏 (𝑓𝑡) = ran 𝑓)
9669, 73, 953syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑡𝑏 (𝑓𝑡) = ran 𝑓)
9794, 96sseqtrd 3984 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 ran 𝑓)
9889, 97eqsstrd 3982 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 ran 𝑓)
99 simpll2 1213 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑐𝐽)
10071, 99sstrd 3954 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝐽)
101 uniss 4873 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑓𝐽 ran 𝑓 𝐽)
102101, 1sseqtrrdi 3995 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑓𝐽 ran 𝑓𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑋)
10498, 103eqssd 3961 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 = ran 𝑓)
105 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
106105eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = ran 𝑓 → (𝑋 = 𝑑𝑋 = ran 𝑓))
107106rspcev 3581 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
10888, 104, 107syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
109108exp32 421 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
110109exlimdv 1936 . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . 13 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
11755, 116syld 47 . . . . . . . . . . . 12 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
1181173exp 1119 . . . . . . . . . . 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 3149 . . . . . . 7 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
123 fibas 22327 . . . . . . . . 9 (fi‘𝑥) ∈ TopBases
124 tgcl 22319 . . . . . . . . 9 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125123, 124ax-mp 5 . . . . . . . 8 (topGen‘(fi‘𝑥)) ∈ Top
126 eleq1 2825 . . . . . . . 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 22739 . . . . . 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 1933 . 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 1087   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  {crab 3407  cin 3909  wss 3910  𝒫 cpw 4560   cuni 4865   ciun 4954   class class class wbr 5105  ran crn 5634   Fn wfn 6491  wf 6492  ontowfo 6494  cfv 6496  cdom 8881  Fincfn 8883  ficfi 9346  topGenctg 17319  Topctop 22242  TopBasesctb 22295  Compccmp 22737
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-ac2 10399
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-rpss 7660  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887  df-fi 9347  df-card 9875  df-ac 10052  df-topgen 17325  df-top 22243  df-bases 22296  df-cmp 22738
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator