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

Theorem alexsubALT 22634
 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 22630 . 2 (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
31alexsubALTlem4 22633 . . . . 5 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
4 velpw 4517 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
5 eleq2 2900 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑐 → (𝑡𝑋𝑡 𝑐))
653ad2ant3 1132 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋𝑡 𝑐))
7 eluni 4814 . . . . . . . . . . . . . . . . . . . 20 (𝑡 𝑐 ↔ ∃𝑤(𝑡𝑤𝑤𝑐))
8 ssel 3937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐𝐽 → (𝑤𝑐𝑤𝐽))
9 eleq2 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤𝐽𝑤 ∈ (topGen‘(fi‘𝑥))))
10 tg2 21548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤 ∈ (topGen‘(fi‘𝑥)) ∧ 𝑡𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤))
1110ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (topGen‘(fi‘𝑥)) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤)))
129, 11syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤𝐽 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤))))
138, 12sylan9r 512 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑤𝑐 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤))))
14133impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤)))
15 sseq2 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑤 → (𝑦𝑧𝑦𝑤))
1615rspcev 3600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤𝑐𝑦𝑤) → ∃𝑧𝑐 𝑦𝑧)
1716ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑐 → (𝑦𝑤 → ∃𝑧𝑐 𝑦𝑧))
18173ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑦𝑤 → ∃𝑧𝑐 𝑦𝑧))
1918anim2d 614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → ((𝑡𝑦𝑦𝑤) → (𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2019reximdv 3259 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦𝑦𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2114, 20syld 47 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑤𝑐) → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
22213expia 1118 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑤𝑐 → (𝑡𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))))
2322com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑡𝑤 → (𝑤𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))))
2423impd 414 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → ((𝑡𝑤𝑤𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
2524exlimdv 1935 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (∃𝑤(𝑡𝑤𝑤𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
267, 25syl5bi 245 . . . . . . . . . . . . . . . . . . 19 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽) → (𝑡 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
27263adant3 1129 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
286, 27sylbid 243 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
29 ssel 3937 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑧 → (𝑡𝑦𝑡𝑧))
30 elunii 4816 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡𝑧𝑧𝑐) → 𝑡 𝑐)
3130expcom 417 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑐 → (𝑡𝑧𝑡 𝑐))
326biimprd 251 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡 𝑐𝑡𝑋))
3331, 32sylan9r 512 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑧𝑐) → (𝑡𝑧𝑡𝑋))
3429, 33syl9r 78 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑧𝑐) → (𝑦𝑧 → (𝑡𝑦𝑡𝑋)))
3534rexlimdva 3270 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑧𝑐 𝑦𝑧 → (𝑡𝑦𝑡𝑋)))
3635com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑦 → (∃𝑧𝑐 𝑦𝑧𝑡𝑋)))
3736impd 414 . . . . . . . . . . . . . . . . . 18 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → ((𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧) → 𝑡𝑋))
3837rexlimdvw 3276 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧) → 𝑡𝑋))
3928, 38impbid 215 . . . . . . . . . . . . . . . 16 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧)))
40 elunirab 4827 . . . . . . . . . . . . . . . 16 (𝑡 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡𝑦 ∧ ∃𝑧𝑐 𝑦𝑧))
4139, 40syl6bbr 292 . . . . . . . . . . . . . . 15 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑡𝑋𝑡 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
4241eqrdv 2819 . . . . . . . . . . . . . 14 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → 𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
43 ssrab2 4032 . . . . . . . . . . . . . . . 16 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ⊆ (fi‘𝑥)
44 fvex 6656 . . . . . . . . . . . . . . . . 17 (fi‘𝑥) ∈ V
4544elpw2 5221 . . . . . . . . . . . . . . . 16 ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ⊆ (fi‘𝑥))
4643, 45mpbir 234 . . . . . . . . . . . . . . 15 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∈ 𝒫 (fi‘𝑥)
47 unieq 4822 . . . . . . . . . . . . . . . . . 18 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → 𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
4847eqeq2d 2832 . . . . . . . . . . . . . . . . 17 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑎𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
49 pweq 4528 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧})
5049ineq1d 4163 . . . . . . . . . . . . . . . . . 18 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin))
5150rexeqdv 3397 . . . . . . . . . . . . . . . . 17 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏))
5248, 51imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ((𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ (𝑋 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏)))
5352rspcv 3595 . . . . . . . . . . . . . . 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 8802 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∧ 𝑏 ∈ Fin))
57 ssel 3937 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑡𝑏𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧}))
58 sseq1 3968 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑡 → (𝑦𝑧𝑡𝑧))
5958rexbidv 3283 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑡 → (∃𝑧𝑐 𝑦𝑧 ↔ ∃𝑧𝑐 𝑡𝑧))
6059elrab 3657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧𝑐 𝑡𝑧))
6160simprbi 500 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑧𝑐 𝑡𝑧)
6257, 61syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑡𝑏 → ∃𝑧𝑐 𝑡𝑧))
6362ralrimiv 3169 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∀𝑡𝑏𝑧𝑐 𝑡𝑧)
64 sseq2 3969 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑓𝑡) → (𝑡𝑧𝑡 ⊆ (𝑓𝑡)))
6564ac6sfi 8738 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ Fin ∧ ∀𝑡𝑏𝑧𝑐 𝑡𝑧) → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)))
6665ex 416 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ Fin → (∀𝑡𝑏𝑧𝑐 𝑡𝑧 → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
6763, 66syl5 34 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
6867adantl 485 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → ∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))))
69 simprll 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑓:𝑏𝑐)
70 frn 6493 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑏𝑐 → ran 𝑓𝑐)
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑐)
72 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 ∈ Fin)
73 ffn 6487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:𝑏𝑐𝑓 Fn 𝑏)
74 dffn4 6569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn 𝑏𝑓:𝑏onto→ran 𝑓)
7573, 74sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑏𝑐𝑓:𝑏onto→ran 𝑓)
7675adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → 𝑓:𝑏onto→ran 𝑓)
7776ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑓:𝑏onto→ran 𝑓)
78 fodomfi 8773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏 ∈ Fin ∧ 𝑓:𝑏onto→ran 𝑓) → ran 𝑓𝑏)
7972, 77, 78syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑏)
80 domfi 8715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∈ Fin ∧ ran 𝑓𝑏) → ran 𝑓 ∈ Fin)
8172, 79, 80syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓 ∈ Fin)
8271, 81jca 515 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → (ran 𝑓𝑐 ∧ ran 𝑓 ∈ Fin))
83 elin 3926 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84 vex 3474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑐 ∈ V
8584elpw2 5221 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
8685anbi1i 626 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ (ran 𝑓𝑐 ∧ ran 𝑓 ∈ Fin))
8783, 86bitr2i 279 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑓𝑐 ∧ ran 𝑓 ∈ Fin) ↔ ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
8882, 87sylib 221 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
89 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 = 𝑏)
90 uniiun 4955 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏 = 𝑡𝑏 𝑡
91 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡))
92 ss2iun 4910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡) → 𝑡𝑏 𝑡 𝑡𝑏 (𝑓𝑡))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑡𝑏 𝑡 𝑡𝑏 (𝑓𝑡))
9490, 93eqsstrid 3991 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 𝑡𝑏 (𝑓𝑡))
95 fniunfv 6980 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑏 𝑡𝑏 (𝑓𝑡) = ran 𝑓)
9669, 73, 953syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑡𝑏 (𝑓𝑡) = ran 𝑓)
9794, 96sseqtrd 3983 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑏 ran 𝑓)
9889, 97eqsstrd 3981 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 ran 𝑓)
99 simpll2 1210 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑐𝐽)
10071, 99sstrd 3953 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝐽)
101 uniss 4819 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑓𝐽 ran 𝑓 𝐽)
102101, 1sseqtrrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑓𝐽 ran 𝑓𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ran 𝑓𝑋)
10498, 103eqssd 3960 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → 𝑋 = ran 𝑓)
105 unieq 4822 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
106105eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = ran 𝑓 → (𝑋 = 𝑑𝑋 = ran 𝑓))
107106rspcev 3600 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
10888, 104, 107syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) ∧ 𝑋 = 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
109108exp32 424 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
110109exlimdv 1935 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (∃𝑓(𝑓:𝑏𝑐 ∧ ∀𝑡𝑏 𝑡 ⊆ (𝑓𝑡)) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
11168, 110syld 47 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
112111ex 416 . . . . . . . . . . . . . . . . 17 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
113112com23 86 . . . . . . . . . . . . . . . 16 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} → (𝑏 ∈ Fin → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
114113impd 414 . . . . . . . . . . . . . . 15 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → ((𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∧ 𝑏 ∈ Fin) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
11556, 114syl5bi 245 . . . . . . . . . . . . . 14 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin) → (𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
116115rexlimdv 3269 . . . . . . . . . . . . 13 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧𝑐 𝑦𝑧} ∩ Fin)𝑋 = 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
11755, 116syld 47 . . . . . . . . . . . 12 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐𝐽𝑋 = 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
1181173exp 1116 . . . . . . . . . . 11 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐𝐽 → (𝑋 = 𝑐 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
119118com34 91 . . . . . . . . . 10 (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐𝐽 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
120119com23 86 . . . . . . . . 9 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑐𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
1214, 120syl7bi 258 . . . . . . . 8 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
122121ralrimdv 3176 . . . . . . 7 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
123 fibas 21560 . . . . . . . . 9 (fi‘𝑥) ∈ TopBases
124 tgcl 21552 . . . . . . . . 9 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125123, 124ax-mp 5 . . . . . . . 8 (topGen‘(fi‘𝑥)) ∈ Top
126 eleq1 2899 . . . . . . . 8 (𝐽 = (topGen‘(fi‘𝑥)) → (𝐽 ∈ Top ↔ (topGen‘(fi‘𝑥)) ∈ Top))
127125, 126mpbiri 261 . . . . . . 7 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 ∈ Top)
128122, 127jctild 529 . . . . . 6 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))))
1291iscmp 21971 . . . . . 6 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
130128, 129syl6ibr 255 . . . . 5 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) → 𝐽 ∈ Comp))
1313, 130syld 47 . . . 4 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → 𝐽 ∈ Comp))
132131imp 410 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)) → 𝐽 ∈ Comp)
133132exlimiv 1932 . 2 (∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)) → 𝐽 ∈ Comp)
1342, 133impbii 212 1 (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115  ∀wral 3126  ∃wrex 3127  {crab 3130   ∩ cin 3909   ⊆ wss 3910  𝒫 cpw 4512  ∪ cuni 4811  ∪ ciun 4892   class class class wbr 5039  ran crn 5529   Fn wfn 6323  ⟶wf 6324  –onto→wfo 6326  ‘cfv 6328   ≼ cdom 8482  Fincfn 8484  ficfi 8850  topGenctg 16689  Topctop 21476  TopBasesctb 21528  Compccmp 21969 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-ac2 9862 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-rpss 7424  df-om 7556  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-oadd 8081  df-er 8264  df-en 8485  df-dom 8486  df-fin 8488  df-fi 8851  df-card 9344  df-ac 9519  df-topgen 16695  df-top 21477  df-bases 21529  df-cmp 21970 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator