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

Theorem alexsubALTlem4 24073
Description: Lemma for alexsubALT 24074. 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 3069 . . . . 5 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2 alexsubALT.1 . . . . . . . 8 𝑋 = 𝐽
32alexsubALTlem2 24071 . . . . . . 7 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣)
4 elun 4162 . . . . . . . . . 10 (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ↔ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∨ 𝑢 ∈ {∅}))
5 sseq2 4021 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝑎𝑧𝑎𝑢))
6 pweq 4618 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢)
76ineq1d 4226 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑢 ∩ Fin))
87raleqdv 3323 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
95, 8anbi12d 632 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)))
109elrab 3694 . . . . . . . . . . 11 (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)))
11 velsn 4646 . . . . . . . . . . 11 (𝑢 ∈ {∅} ↔ 𝑢 = ∅)
1210, 11orbi12i 914 . . . . . . . . . 10 ((𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∨ 𝑢 ∈ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅))
134, 12bitri 275 . . . . . . . . 9 (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅))
14 ralnex 3069 . . . . . . . . . . . . 13 (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 ↔ ¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
15 simprrl 781 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑎𝑢)
1615unissd 4921 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑎 𝑢)
17 sseq1 4020 . . . . . . . . . . . . . . . 16 (𝑋 = 𝑎 → (𝑋 𝑢 𝑎 𝑢))
1816, 17syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = 𝑎𝑋 𝑢))
19 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ∈ V
20 inss1 4244 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑢) ⊆ 𝑥
2119, 20elpwi2 5340 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝑢) ∈ 𝒫 𝑥
22 unieq 4922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (𝑥𝑢) → 𝑐 = (𝑥𝑢))
2322eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (𝑥𝑢) → (𝑋 = 𝑐𝑋 = (𝑥𝑢)))
24 pweq 4618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = (𝑥𝑢) → 𝒫 𝑐 = 𝒫 (𝑥𝑢))
2524ineq1d 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (𝑥𝑢) → (𝒫 𝑐 ∩ Fin) = (𝒫 (𝑥𝑢) ∩ Fin))
2625rexeqdv 3324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (𝑥𝑢) → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 ↔ ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑))
2723, 26imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (𝑥𝑢) → ((𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ↔ (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑)))
2827rspccv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ((𝑥𝑢) ∈ 𝒫 𝑥 → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑)))
2921, 28mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑))
30 inss2 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝑢) ⊆ 𝑢
31 sstr 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑑 ⊆ (𝑥𝑢) ∧ (𝑥𝑢) ⊆ 𝑢) → 𝑑𝑢)
3230, 31mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 ⊆ (𝑥𝑢) → 𝑑𝑢)
3332anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑑 ⊆ (𝑥𝑢) ∧ 𝑑 ∈ Fin) → (𝑑𝑢𝑑 ∈ Fin))
34 elfpw 9391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) ↔ (𝑑 ⊆ (𝑥𝑢) ∧ 𝑑 ∈ Fin))
35 elfpw 9391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ↔ (𝑑𝑢𝑑 ∈ Fin))
3633, 34, 353imtr4i 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) → 𝑑 ∈ (𝒫 𝑢 ∩ Fin))
3736anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = 𝑑))
3837reximi2 3076 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑)
3929, 38syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑))
40 unieq 4922 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 𝑑 = 𝑏)
4140eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = 𝑏 → (𝑋 = 𝑑𝑋 = 𝑏))
4241cbvrexvw 3235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑 ↔ ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
4339, 42imbitrdi 251 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
44 dfrex2 3070 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
4543, 44imbitrdi 251 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
4645con2d 134 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢)))
4746a1d 25 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
48473ad2ant2 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
4948adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
5049impd 410 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → ((𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏) → ¬ 𝑋 = (𝑥𝑢)))
5150impr 454 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → ¬ 𝑋 = (𝑥𝑢))
5220unissi 4920 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑢) ⊆ 𝑥
53 fiuni 9465 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
5453elv 3482 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 = (fi‘𝑥)
55 fibas 22999 . . . . . . . . . . . . . . . . . . . . . . . . 25 (fi‘𝑥) ∈ TopBases
56 unitg 22989 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘(fi‘𝑥)) = (fi‘𝑥)
5854, 57eqtr4i 2765 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 = (topGen‘(fi‘𝑥))
59 unieq 4922 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6058, 59eqtr4id 2793 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝑥 = 𝐽)
6160, 2eqtr4di 2792 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 = (topGen‘(fi‘𝑥)) → 𝑥 = 𝑋)
62613ad2ant1 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝑥 = 𝑋)
6362adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑥 = 𝑋)
6452, 63sseqtrid 4047 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑥𝑢) ⊆ 𝑋)
65 eqcom 2741 . . . . . . . . . . . . . . . . . . 19 (𝑋 = (𝑥𝑢) ↔ (𝑥𝑢) = 𝑋)
66 eqss 4010 . . . . . . . . . . . . . . . . . . . 20 ( (𝑥𝑢) = 𝑋 ↔ ( (𝑥𝑢) ⊆ 𝑋𝑋 (𝑥𝑢)))
6766baib 535 . . . . . . . . . . . . . . . . . . 19 ( (𝑥𝑢) ⊆ 𝑋 → ( (𝑥𝑢) = 𝑋𝑋 (𝑥𝑢)))
6865, 67bitrid 283 . . . . . . . . . . . . . . . . . 18 ( (𝑥𝑢) ⊆ 𝑋 → (𝑋 = (𝑥𝑢) ↔ 𝑋 (𝑥𝑢)))
6964, 68syl 17 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = (𝑥𝑢) ↔ 𝑋 (𝑥𝑢)))
7051, 69mtbid 324 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → ¬ 𝑋 (𝑥𝑢))
71 sstr2 4001 . . . . . . . . . . . . . . . . 17 (𝑋 𝑢 → ( 𝑢 (𝑥𝑢) → 𝑋 (𝑥𝑢)))
7271con3rr3 155 . . . . . . . . . . . . . . . 16 𝑋 (𝑥𝑢) → (𝑋 𝑢 → ¬ 𝑢 (𝑥𝑢)))
7370, 72syl 17 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 𝑢 → ¬ 𝑢 (𝑥𝑢)))
74 nss 4059 . . . . . . . . . . . . . . . . 17 𝑢 (𝑥𝑢) ↔ ∃𝑦(𝑦 𝑢 ∧ ¬ 𝑦 (𝑥𝑢)))
75 df-rex 3068 . . . . . . . . . . . . . . . . 17 (∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢) ↔ ∃𝑦(𝑦 𝑢 ∧ ¬ 𝑦 (𝑥𝑢)))
7674, 75bitr4i 278 . . . . . . . . . . . . . . . 16 𝑢 (𝑥𝑢) ↔ ∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢))
77 eluni2 4915 . . . . . . . . . . . . . . . . . 18 (𝑦 𝑢 ↔ ∃𝑤𝑢 𝑦𝑤)
78 elpwi 4611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
7978sseld 3993 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑤𝑢𝑤 ∈ (fi‘𝑥)))
8079ad2antrl 728 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢𝑤 ∈ (fi‘𝑥)))
81 elfi 9450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 ∈ V ∧ 𝑥 ∈ V) → (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡))
8281el2v 3484 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡)
8380, 82imbitrdi 251 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡))
842alexsubALTlem3 24072 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
8578adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → 𝑢 ⊆ (fi‘𝑥))
8685ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ⊆ (fi‘𝑥))
87 ssfii 9456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ V → 𝑥 ⊆ (fi‘𝑥))
8887elv 3482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑥 ⊆ (fi‘𝑥)
89 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
9089elpwid 4613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
9190ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → 𝑡𝑥)
9291ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑡𝑥)
93 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠𝑡)
9492, 93sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠𝑥)
9588, 94sselid 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠 ∈ (fi‘𝑥))
9695snssd 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → {𝑠} ⊆ (fi‘𝑥))
9786, 96unssd 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
98 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (fi‘𝑥) ∈ V
9998elpw2 5339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ↔ (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
10097, 99sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥))
101 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → 𝑎𝑢)
102101ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑎𝑢)
103 ssun1 4187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑢 ⊆ (𝑢 ∪ {𝑠})
104102, 103sstrdi 4007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑎 ⊆ (𝑢 ∪ {𝑠}))
105 unieq 4922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑏 𝑛 = 𝑏)
106105eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑏 → (𝑋 = 𝑛𝑋 = 𝑏))
107106notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑏 → (¬ 𝑋 = 𝑛 ↔ ¬ 𝑋 = 𝑏))
108107cbvralvw 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)
109108biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)
110109ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)
111100, 104, 110jca32 515 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
112 sseq2 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑢 ∪ {𝑠}) → (𝑎𝑧𝑎 ⊆ (𝑢 ∪ {𝑠})))
113 pweq 4618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑢 ∪ {𝑠}) → 𝒫 𝑧 = 𝒫 (𝑢 ∪ {𝑠}))
114113ineq1d 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑢 ∪ {𝑠}) → (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin))
115114raleqdv 3323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑢 ∪ {𝑠}) → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏))
116112, 115anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = (𝑢 ∪ {𝑠}) → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
117116elrab 3694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
118111, 117sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)})
119 elun1 4191 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
121 vsnid 4667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ {𝑠}
122 elun2 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ {𝑠} → 𝑠 ∈ (𝑢 ∪ {𝑠}))
123121, 122ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑠 ∈ (𝑢 ∪ {𝑠})
124 intss1 4967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑠𝑡 𝑡𝑠)
125 sseq1 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑤 = 𝑡 → (𝑤𝑠 𝑡𝑠))
126124, 125syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑠𝑡 → (𝑤 = 𝑡𝑤𝑠))
127126impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑤 = 𝑡𝑠𝑡) → 𝑤𝑠)
128127ad4ant24 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ 𝑠𝑡) → 𝑤𝑠)
129128adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑤𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ 𝑠𝑡)) → 𝑤𝑠)
130129adantrrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑤𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑤𝑠)
131130adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑤𝑠)
132 simprlr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑦𝑤)
133131, 132sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑦𝑠)
13490ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) → 𝑡𝑥)
135134ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑡𝑥)
136 simprrl 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑠𝑡)
137135, 136sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑠𝑥)
138 elin 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ (𝑥𝑢) ↔ (𝑠𝑥𝑠𝑢))
139 elunii 4916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦𝑠𝑠 ∈ (𝑥𝑢)) → 𝑦 (𝑥𝑢))
140139ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦𝑠 → (𝑠 ∈ (𝑥𝑢) → 𝑦 (𝑥𝑢)))
141138, 140biimtrrid 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦𝑠 → ((𝑠𝑥𝑠𝑢) → 𝑦 (𝑥𝑢)))
142141expd 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦𝑠 → (𝑠𝑥 → (𝑠𝑢𝑦 (𝑥𝑢))))
143133, 137, 142sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → (𝑠𝑢𝑦 (𝑥𝑢)))
144143con3d 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → (¬ 𝑦 (𝑥𝑢) → ¬ 𝑠𝑢))
145144expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤)) → ((𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛) → (¬ 𝑦 (𝑥𝑢) → ¬ 𝑠𝑢)))
146145com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤)) → (¬ 𝑦 (𝑥𝑢) → ((𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛) → ¬ 𝑠𝑢)))
147146exp32 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ((𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛) → ¬ 𝑠𝑢)))))
148147imp55 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ¬ 𝑠𝑢)
149 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ V
150 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 → (𝑣 ∈ (𝑢 ∪ {𝑠}) ↔ 𝑠 ∈ (𝑢 ∪ {𝑠})))
151 elequ1 2112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = 𝑠 → (𝑣𝑢𝑠𝑢))
152151notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 → (¬ 𝑣𝑢 ↔ ¬ 𝑠𝑢))
153150, 152anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = 𝑠 → ((𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢) ↔ (𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠𝑢)))
154149, 153spcev 3605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠𝑢) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
155123, 148, 154sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
156 nss 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 ↔ ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
157155, 156sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢)
158 eqimss2 4054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = (𝑢 ∪ {𝑠}) → (𝑢 ∪ {𝑠}) ⊆ 𝑢)
159158necon3bi 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢𝑢 ≠ (𝑢 ∪ {𝑠}))
160157, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ≠ (𝑢 ∪ {𝑠}))
161160, 103jctil 519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
162 df-pss 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ⊊ (𝑢 ∪ {𝑠}) ↔ (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
163161, 162sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ⊊ (𝑢 ∪ {𝑠}))
164 psseq2 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = (𝑢 ∪ {𝑠}) → (𝑢𝑣𝑢 ⊊ (𝑢 ∪ {𝑠})))
165164rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ∧ 𝑢 ⊊ (𝑢 ∪ {𝑠})) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
166120, 163, 165syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
16784, 166rexlimddv 3158 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
168167exp45 438 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))))
169168expd 415 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → (𝑤 = 𝑡 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))))
170169rexlimdv 3150 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))))
171170ex 412 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))))
17283, 171mpdd 43 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))))
173172rexlimdv 3150 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∃𝑤𝑢 𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))
17477, 173biimtrid 242 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑦 𝑢 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))
175174rexlimdv 3150 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))
17676, 175biimtrid 242 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (¬ 𝑢 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))
17718, 73, 1763syld 60 . . . . . . . . . . . . . 14 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = 𝑎 → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣))
178177con3d 152 . . . . . . . . . . . . 13 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣 → ¬ 𝑋 = 𝑎))
17914, 178biimtrid 242 . . . . . . . . . . . 12 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎))
180179ex 412 . . . . . . . . . . 11 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
181180adantr 480 . . . . . . . . . 10 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
182 ssun1 4187 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})
183 eqimss2 4054 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎𝑎𝑧)
184183biantrurd 532 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)))
185 pweq 4618 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎)
186185ineq1d 4226 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑎 ∩ Fin))
187186raleqdv 3323 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
188184, 187bitr3d 281 . . . . . . . . . . . . . . 15 (𝑧 = 𝑎 → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
189 simpll3 1213 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ 𝒫 (fi‘𝑥))
190 simplr 769 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏)
191188, 189, 190elrabd 3696 . . . . . . . . . . . . . 14 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)})
192182, 191sselid 3992 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
193 psseq2 4100 . . . . . . . . . . . . . . 15 (𝑣 = 𝑎 → (𝑢𝑣𝑢𝑎))
194193notbid 318 . . . . . . . . . . . . . 14 (𝑣 = 𝑎 → (¬ 𝑢𝑣 ↔ ¬ 𝑢𝑎))
195194rspcv 3617 . . . . . . . . . . . . 13 (𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑢𝑎))
196192, 195syl 17 . . . . . . . . . . . 12 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑢𝑎))
197 id 22 . . . . . . . . . . . . . . . . 17 (𝑎 = ∅ → 𝑎 = ∅)
198 0elpw 5361 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑎
199 0fi 9080 . . . . . . . . . . . . . . . . . 18 ∅ ∈ Fin
200198, 199elini 4208 . . . . . . . . . . . . . . . . 17 ∅ ∈ (𝒫 𝑎 ∩ Fin)
201197, 200eqeltrdi 2846 . . . . . . . . . . . . . . . 16 (𝑎 = ∅ → 𝑎 ∈ (𝒫 𝑎 ∩ Fin))
202 unieq 4922 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑎 𝑏 = 𝑎)
203202eqeq2d 2745 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑎 → (𝑋 = 𝑏𝑋 = 𝑎))
204203notbid 318 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑎 → (¬ 𝑋 = 𝑏 ↔ ¬ 𝑋 = 𝑎))
205204rspccv 3618 . . . . . . . . . . . . . . . 16 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑎 ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = 𝑎))
206201, 205syl5 34 . . . . . . . . . . . . . . 15 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑎 = ∅ → ¬ 𝑋 = 𝑎))
207206necon2ad 2952 . . . . . . . . . . . . . 14 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑋 = 𝑎𝑎 ≠ ∅))
208207ad2antlr 727 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑋 = 𝑎𝑎 ≠ ∅))
209 psseq1 4099 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢𝑎 ↔ ∅ ⊊ 𝑎))
210209adantl 481 . . . . . . . . . . . . . 14 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑢𝑎 ↔ ∅ ⊊ 𝑎))
211 0pss 4452 . . . . . . . . . . . . . 14 (∅ ⊊ 𝑎𝑎 ≠ ∅)
212210, 211bitrdi 287 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑢𝑎𝑎 ≠ ∅))
213208, 212sylibrd 259 . . . . . . . . . . . 12 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑋 = 𝑎𝑢𝑎))
214196, 213nsyld 156 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎))
215214ex 412 . . . . . . . . . 10 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (𝑢 = ∅ → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
216181, 215jaod 859 . . . . . . . . 9 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
21713, 216biimtrid 242 . . . . . . . 8 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎)))
218217rexlimdv 3150 . . . . . . 7 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → (∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 → ¬ 𝑋 = 𝑎))
2193, 218mpd 15 . . . . . 6 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ¬ 𝑋 = 𝑎)
220219ex 412 . . . . 5 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = 𝑎))
2211, 220biimtrrid 243 . . . 4 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏 → ¬ 𝑋 = 𝑎))
222221con4d 115 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
2232223exp 1118 . 2 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑎 ∈ 𝒫 (fi‘𝑥) → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
224223ralrimdv 3149 1 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cun 3960  cin 3961  wss 3962  wpss 3963  c0 4338  𝒫 cpw 4604  {csn 4630   cuni 4911   cint 4950  cfv 6562  Fincfn 8983  ficfi 9447  topGenctg 17483  TopBasesctb 22967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-ac2 10500
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-rpss 7741  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-1o 8504  df-2o 8505  df-en 8984  df-fin 8987  df-fi 9448  df-card 9976  df-ac 10153  df-topgen 17489  df-bases 22968
This theorem is referenced by:  alexsubALT  24074
  Copyright terms: Public domain W3C validator