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

Theorem alexsubALTlem4 22088
Description: Lemma for alexsubALT 22089. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
Hypothesis
Ref Expression
alexsubALT.1 𝑋 = 𝐽
Assertion
Ref Expression
alexsubALTlem4 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝐽   𝑋,𝑎,𝑏,𝑐,𝑑,𝑥

Proof of Theorem alexsubALTlem4
Dummy variables 𝑛 𝑠 𝑡 𝑢 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralnex 3191 . . . . 5 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2 alexsubALT.1 . . . . . . . 8 𝑋 = 𝐽
32alexsubALTlem2 22086 . . . . . . 7 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣)
4 elun 3963 . . . . . . . . . 10 (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ↔ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∨ 𝑢 ∈ {∅}))
5 sseq2 3835 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝑎𝑧𝑎𝑢))
6 pweq 4365 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢)
76ineq1d 4023 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑢 ∩ Fin))
87raleqdv 3344 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
95, 8anbi12d 618 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)))
109elrab 3570 . . . . . . . . . . 11 (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)))
11 velsn 4397 . . . . . . . . . . 11 (𝑢 ∈ {∅} ↔ 𝑢 = ∅)
1210, 11orbi12i 929 . . . . . . . . . 10 ((𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∨ 𝑢 ∈ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅))
134, 12bitri 266 . . . . . . . . 9 (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅))
14 ralnex 3191 . . . . . . . . . . . . 13 (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 ↔ ¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
15 simprrl 790 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑎𝑢)
1615unissd 4667 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑎 𝑢)
17 sseq1 3834 . . . . . . . . . . . . . . . 16 (𝑋 = 𝑎 → (𝑋 𝑢 𝑎 𝑢))
1816, 17syl5ibrcom 238 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = 𝑎𝑋 𝑢))
19 inss1 4040 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑢) ⊆ 𝑥
20 vex 3405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑥 ∈ V
2120elpw2 5033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥𝑢) ∈ 𝒫 𝑥 ↔ (𝑥𝑢) ⊆ 𝑥)
2219, 21mpbir 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝑢) ∈ 𝒫 𝑥
23 unieq 4649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (𝑥𝑢) → 𝑐 = (𝑥𝑢))
2423eqeq2d 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (𝑥𝑢) → (𝑋 = 𝑐𝑋 = (𝑥𝑢)))
25 pweq 4365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = (𝑥𝑢) → 𝒫 𝑐 = 𝒫 (𝑥𝑢))
2625ineq1d 4023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (𝑥𝑢) → (𝒫 𝑐 ∩ Fin) = (𝒫 (𝑥𝑢) ∩ Fin))
2726rexeqdv 3345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (𝑥𝑢) → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 ↔ ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑))
2824, 27imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (𝑥𝑢) → ((𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ↔ (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑)))
2928rspccv 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ((𝑥𝑢) ∈ 𝒫 𝑥 → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑)))
3022, 29mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑))
31 inss2 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝑢) ⊆ 𝑢
32 sstr 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑑 ⊆ (𝑥𝑢) ∧ (𝑥𝑢) ⊆ 𝑢) → 𝑑𝑢)
3331, 32mpan2 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 ⊆ (𝑥𝑢) → 𝑑𝑢)
3433anim1i 604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑑 ⊆ (𝑥𝑢) ∧ 𝑑 ∈ Fin) → (𝑑𝑢𝑑 ∈ Fin))
35 elfpw 8517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) ↔ (𝑑 ⊆ (𝑥𝑢) ∧ 𝑑 ∈ Fin))
36 elfpw 8517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ↔ (𝑑𝑢𝑑 ∈ Fin))
3734, 35, 363imtr4i 283 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) → 𝑑 ∈ (𝒫 𝑢 ∩ Fin))
3837anim1i 604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = 𝑑))
3938reximi2 3208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑)
4030, 39syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑))
41 unieq 4649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 𝑑 = 𝑏)
4241eqeq2d 2827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = 𝑏 → (𝑋 = 𝑑𝑋 = 𝑏))
4342cbvrexv 3372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑 ↔ ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
4440, 43syl6ib 242 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
45 dfrex2 3194 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
4644, 45syl6ib 242 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
4746con2d 131 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢)))
4847a1d 25 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
49483ad2ant2 1157 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
5049adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
5150impd 398 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → ((𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏) → ¬ 𝑋 = (𝑥𝑢)))
5251impr 444 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → ¬ 𝑋 = (𝑥𝑢))
5319unissi 4666 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑢) ⊆ 𝑥
54 unieq 4649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
55 fiuni 8583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
5620, 55ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 = (fi‘𝑥)
57 fibas 21016 . . . . . . . . . . . . . . . . . . . . . . . . 25 (fi‘𝑥) ∈ TopBases
58 unitg 21006 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
5957, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘(fi‘𝑥)) = (fi‘𝑥)
6056, 59eqtr4i 2842 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 = (topGen‘(fi‘𝑥))
6154, 60syl6reqr 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝑥 = 𝐽)
6261, 2syl6eqr 2869 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 = (topGen‘(fi‘𝑥)) → 𝑥 = 𝑋)
63623ad2ant1 1156 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝑥 = 𝑋)
6463adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑥 = 𝑋)
6553, 64syl5sseq 3861 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑥𝑢) ⊆ 𝑋)
66 eqcom 2824 . . . . . . . . . . . . . . . . . . 19 (𝑋 = (𝑥𝑢) ↔ (𝑥𝑢) = 𝑋)
67 eqss 3824 . . . . . . . . . . . . . . . . . . . 20 ( (𝑥𝑢) = 𝑋 ↔ ( (𝑥𝑢) ⊆ 𝑋𝑋 (𝑥𝑢)))
6867baib 527 . . . . . . . . . . . . . . . . . . 19 ( (𝑥𝑢) ⊆ 𝑋 → ( (𝑥𝑢) = 𝑋𝑋 (𝑥𝑢)))
6966, 68syl5bb 274 . . . . . . . . . . . . . . . . . 18 ( (𝑥𝑢) ⊆ 𝑋 → (𝑋 = (𝑥𝑢) ↔ 𝑋 (𝑥𝑢)))
7065, 69syl 17 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = (𝑥𝑢) ↔ 𝑋 (𝑥𝑢)))
7152, 70mtbid 315 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → ¬ 𝑋 (𝑥𝑢))
72 sstr2 3816 . . . . . . . . . . . . . . . . 17 (𝑋 𝑢 → ( 𝑢 (𝑥𝑢) → 𝑋 (𝑥𝑢)))
7372con3rr3 152 . . . . . . . . . . . . . . . 16 𝑋 (𝑥𝑢) → (𝑋 𝑢 → ¬ 𝑢 (𝑥𝑢)))
7471, 73syl 17 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 𝑢 → ¬ 𝑢 (𝑥𝑢)))
75 nss 3871 . . . . . . . . . . . . . . . . 17 𝑢 (𝑥𝑢) ↔ ∃𝑦(𝑦 𝑢 ∧ ¬ 𝑦 (𝑥𝑢)))
76 df-rex 3113 . . . . . . . . . . . . . . . . 17 (∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢) ↔ ∃𝑦(𝑦 𝑢 ∧ ¬ 𝑦 (𝑥𝑢)))
7775, 76bitr4i 269 . . . . . . . . . . . . . . . 16 𝑢 (𝑥𝑢) ↔ ∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢))
78 eluni2 4645 . . . . . . . . . . . . . . . . . 18 (𝑦 𝑢 ↔ ∃𝑤𝑢 𝑦𝑤)
79 elpwi 4372 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
8079sseld 3808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑤𝑢𝑤 ∈ (fi‘𝑥)))
8180ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢𝑤 ∈ (fi‘𝑥)))
82 vex 3405 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
83 elfi 8568 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 ∈ V ∧ 𝑥 ∈ V) → (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡))
8482, 20, 83mp2an 675 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡)
8581, 84syl6ib 242 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡))
862alexsubALTlem3 22087 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
8779adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → 𝑢 ⊆ (fi‘𝑥))
8887ad4antlr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ⊆ (fi‘𝑥))
89 ssfii 8574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ V → 𝑥 ⊆ (fi‘𝑥))
9020, 89ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑥 ⊆ (fi‘𝑥)
91 inss1 4040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝒫 𝑥 ∩ Fin) ⊆ 𝒫 𝑥
9291sseli 3805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
9392elpwid 4374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
9493ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → 𝑡𝑥)
9594ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑡𝑥)
96 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠𝑡)
9795, 96sseldd 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠𝑥)
9890, 97sseldi 3807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠 ∈ (fi‘𝑥))
9998snssd 4541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → {𝑠} ⊆ (fi‘𝑥))
10088, 99unssd 3999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
101 fvex 6431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (fi‘𝑥) ∈ V
102101elpw2 5033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ↔ (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
103100, 102sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥))
104 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → 𝑎𝑢)
105104ad4antlr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑎𝑢)
106 ssun1 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑢 ⊆ (𝑢 ∪ {𝑠})
107105, 106syl6ss 3821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑎 ⊆ (𝑢 ∪ {𝑠}))
108 unieq 4649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑏 𝑛 = 𝑏)
109108eqeq2d 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑏 → (𝑋 = 𝑛𝑋 = 𝑏))
110109notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑏 → (¬ 𝑋 = 𝑛 ↔ ¬ 𝑋 = 𝑏))
111110cbvralv 3371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)
112111biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)
113112ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)
114103, 107, 113jca32 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
115 sseq2 3835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑢 ∪ {𝑠}) → (𝑎𝑧𝑎 ⊆ (𝑢 ∪ {𝑠})))
116 pweq 4365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑢 ∪ {𝑠}) → 𝒫 𝑧 = 𝒫 (𝑢 ∪ {𝑠}))
117116ineq1d 4023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑢 ∪ {𝑠}) → (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin))
118117raleqdv 3344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑢 ∪ {𝑠}) → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏))
119115, 118anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = (𝑢 ∪ {𝑠}) → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
120119elrab 3570 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
121114, 120sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)})
122 elun1 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
123121, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
124 vsnid 4414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ {𝑠}
125 elun2 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ {𝑠} → 𝑠 ∈ (𝑢 ∪ {𝑠}))
126124, 125ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑠 ∈ (𝑢 ∪ {𝑠})
127 intss1 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑠𝑡 𝑡𝑠)
128 sseq1 3834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑤 = 𝑡 → (𝑤𝑠 𝑡𝑠))
129127, 128syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑠𝑡 → (𝑤 = 𝑡𝑤𝑠))
130129impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑤 = 𝑡𝑠𝑡) → 𝑤𝑠)
131130adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑠𝑡) → 𝑤𝑠)
132131adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ 𝑠𝑡) → 𝑤𝑠)
133132adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑤𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ 𝑠𝑡)) → 𝑤𝑠)
134133adantrrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑤𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑤𝑠)
135134adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑤𝑠)
136 simprlr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑦𝑤)
137135, 136sseldd 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑦𝑠)
13893ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) → 𝑡𝑥)
139138ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑡𝑥)
140 simprrl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑠𝑡)
141139, 140sseldd 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑠𝑥)
142 elin 4006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ (𝑥𝑢) ↔ (𝑠𝑥𝑠𝑢))
143 elunii 4646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦𝑠𝑠 ∈ (𝑥𝑢)) → 𝑦 (𝑥𝑢))
144143ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦𝑠 → (𝑠 ∈ (𝑥𝑢) → 𝑦 (𝑥𝑢)))
145142, 144syl5bir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦𝑠 → ((𝑠𝑥𝑠𝑢) → 𝑦 (𝑥𝑢)))
146145expd 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦𝑠 → (𝑠𝑥 → (𝑠𝑢𝑦 (𝑥𝑢))))
147137, 141, 146sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → (𝑠𝑢𝑦 (𝑥𝑢)))
148147con3d 149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → (¬ 𝑦 (𝑥𝑢) → ¬ 𝑠𝑢))
149148expr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤)) → ((𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛) → (¬ 𝑦 (𝑥𝑢) → ¬ 𝑠𝑢)))
150149com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤)) → (¬ 𝑦 (𝑥𝑢) → ((𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛) → ¬ 𝑠𝑢)))
151150exp32 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ((𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛) → ¬ 𝑠𝑢)))))
152151imp55 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ¬ 𝑠𝑢)
153 vex 3405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ V
154 eleq1w 2879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 → (𝑣 ∈ (𝑢 ∪ {𝑠}) ↔ 𝑠 ∈ (𝑢 ∪ {𝑠})))
155 elequ1 2164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = 𝑠 → (𝑣𝑢𝑠𝑢))
156155notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 → (¬ 𝑣𝑢 ↔ ¬ 𝑠𝑢))
157154, 156anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = 𝑠 → ((𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢) ↔ (𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠𝑢)))
158153, 157spcev 3504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠𝑢) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
159126, 152, 158sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
160 nss 3871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 ↔ ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
161159, 160sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢)
162 eqimss2 3866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = (𝑢 ∪ {𝑠}) → (𝑢 ∪ {𝑠}) ⊆ 𝑢)
163162necon3bi 3015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢𝑢 ≠ (𝑢 ∪ {𝑠}))
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ≠ (𝑢 ∪ {𝑠}))
165164, 106jctil 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
166 df-pss 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ⊊ (𝑢 ∪ {𝑠}) ↔ (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
167165, 166sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ⊊ (𝑢 ∪ {𝑠}))
168 psseq2 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = (𝑢 ∪ {𝑠}) → (𝑢𝑣𝑢 ⊊ (𝑢 ∪ {𝑠})))
169168rspcev 3513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ∧ 𝑢 ⊊ (𝑢 ∪ {𝑠})) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
170123, 167, 169syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
17186, 170rexlimddv 3234 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
172171exp45 427 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))))
173172expd 402 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → (𝑤 = 𝑡 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))))
174173rexlimdv 3229 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))))
175174ex 399 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))))
17685, 175mpdd 43 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))))
177176rexlimdv 3229 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∃𝑤𝑢 𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))
17878, 177syl5bi 233 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑦 𝑢 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))
179178rexlimdv 3229 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))
18077, 179syl5bi 233 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (¬ 𝑢 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))
18118, 74, 1803syld 60 . . . . . . . . . . . . . 14 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = 𝑎 → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))
182181con3d 149 . . . . . . . . . . . . 13 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣 → ¬ 𝑋 = 𝑎))
18314, 182syl5bi 233 . . . . . . . . . . . 12 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎))
184183ex 399 . . . . . . . . . . 11 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
185184adantr 468 . . . . . . . . . 10 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
186 ssun1 3986 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})
187 simpll3 1266 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ 𝒫 (fi‘𝑥))
188 simplr 776 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏)
189 eqimss2 3866 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑎𝑎𝑧)
190189biantrurd 524 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)))
191 pweq 4365 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎)
192191ineq1d 4023 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑎 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑎 ∩ Fin))
193192raleqdv 3344 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
194190, 193bitr3d 272 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
195194elrab 3570 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ (𝑎 ∈ 𝒫 (fi‘𝑥) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
196187, 188, 195sylanbrc 574 . . . . . . . . . . . . . 14 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)})
197186, 196sseldi 3807 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
198 psseq2 3904 . . . . . . . . . . . . . . 15 (𝑣 = 𝑎 → (𝑢𝑣𝑢𝑎))
199198notbid 309 . . . . . . . . . . . . . 14 (𝑣 = 𝑎 → (¬ 𝑢𝑣 ↔ ¬ 𝑢𝑎))
200199rspcv 3509 . . . . . . . . . . . . 13 (𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑢𝑎))
201197, 200syl 17 . . . . . . . . . . . 12 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑢𝑎))
202 id 22 . . . . . . . . . . . . . . . . 17 (𝑎 = ∅ → 𝑎 = ∅)
203 0elpw 5039 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑎
204 0fin 8437 . . . . . . . . . . . . . . . . . 18 ∅ ∈ Fin
205 elin 4006 . . . . . . . . . . . . . . . . . 18 (∅ ∈ (𝒫 𝑎 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin))
206203, 204, 205mpbir2an 693 . . . . . . . . . . . . . . . . 17 ∅ ∈ (𝒫 𝑎 ∩ Fin)
207202, 206syl6eqel 2904 . . . . . . . . . . . . . . . 16 (𝑎 = ∅ → 𝑎 ∈ (𝒫 𝑎 ∩ Fin))
208 unieq 4649 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑎 𝑏 = 𝑎)
209208eqeq2d 2827 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑎 → (𝑋 = 𝑏𝑋 = 𝑎))
210209notbid 309 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑎 → (¬ 𝑋 = 𝑏 ↔ ¬ 𝑋 = 𝑎))
211210rspccv 3510 . . . . . . . . . . . . . . . 16 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑎 ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = 𝑎))
212207, 211syl5 34 . . . . . . . . . . . . . . 15 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑎 = ∅ → ¬ 𝑋 = 𝑎))
213212necon2ad 3004 . . . . . . . . . . . . . 14 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑋 = 𝑎𝑎 ≠ ∅))
214213ad2antlr 709 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑋 = 𝑎𝑎 ≠ ∅))
215 psseq1 3903 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢𝑎 ↔ ∅ ⊊ 𝑎))
216215adantl 469 . . . . . . . . . . . . . 14 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑢𝑎 ↔ ∅ ⊊ 𝑎))
217 0pss 4222 . . . . . . . . . . . . . 14 (∅ ⊊ 𝑎𝑎 ≠ ∅)
218216, 217syl6bb 278 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑢𝑎𝑎 ≠ ∅))
219214, 218sylibrd 250 . . . . . . . . . . . 12 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑋 = 𝑎𝑢𝑎))
220201, 219nsyld 155 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎))
221220ex 399 . . . . . . . . . 10 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (𝑢 = ∅ → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
222185, 221jaod 877 . . . . . . . . 9 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
22313, 222syl5bi 233 . . . . . . . 8 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
224223rexlimdv 3229 . . . . . . 7 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎))
2253, 224mpd 15 . . . . . 6 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ¬ 𝑋 = 𝑎)
226225ex 399 . . . . 5 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = 𝑎))
2271, 226syl5bir 234 . . . 4 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏 → ¬ 𝑋 = 𝑎))
228227con4d 115 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
2292283exp 1141 . 2 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑎 ∈ 𝒫 (fi‘𝑥) → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
230229ralrimdv 3167 1 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wne 2989  wral 3107  wrex 3108  {crab 3111  Vcvv 3402  cun 3778  cin 3779  wss 3780  wpss 3781  c0 4127  𝒫 cpw 4362  {csn 4381   cuni 4641   cint 4680  cfv 6111  Fincfn 8202  ficfi 8565  topGenctg 16323  TopBasesctb 20984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-ac2 9580
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-rpss 7177  df-om 7306  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-oadd 7810  df-er 7989  df-en 8203  df-fin 8206  df-fi 8566  df-card 9058  df-ac 9232  df-topgen 16329  df-bases 20985
This theorem is referenced by:  alexsubALT  22089
  Copyright terms: Public domain W3C validator