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

Theorem alexsubALTlem4 24059
Description: Lemma for alexsubALT 24060. 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 3071 . . . . 5 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2 alexsubALT.1 . . . . . . . 8 𝑋 = 𝐽
32alexsubALTlem2 24057 . . . . . . 7 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣)
4 elun 4152 . . . . . . . . . 10 (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ↔ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∨ 𝑢 ∈ {∅}))
5 sseq2 4009 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝑎𝑧𝑎𝑢))
6 pweq 4613 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢)
76ineq1d 4218 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑢 ∩ Fin))
87raleqdv 3325 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
95, 8anbi12d 632 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)))
109elrab 3691 . . . . . . . . . . 11 (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)))
11 velsn 4641 . . . . . . . . . . 11 (𝑢 ∈ {∅} ↔ 𝑢 = ∅)
1210, 11orbi12i 914 . . . . . . . . . 10 ((𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∨ 𝑢 ∈ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅))
134, 12bitri 275 . . . . . . . . 9 (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) ∨ 𝑢 = ∅))
14 ralnex 3071 . . . . . . . . . . . . 13 (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}) ¬ 𝑢𝑣 ↔ ¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)
15 simprrl 780 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑎𝑢)
1615unissd 4916 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑎 𝑢)
17 sseq1 4008 . . . . . . . . . . . . . . . 16 (𝑋 = 𝑎 → (𝑋 𝑢 𝑎 𝑢))
1816, 17syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 = 𝑎𝑋 𝑢))
19 vex 3483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ∈ V
20 inss1 4236 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑢) ⊆ 𝑥
2119, 20elpwi2 5334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝑢) ∈ 𝒫 𝑥
22 unieq 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (𝑥𝑢) → 𝑐 = (𝑥𝑢))
2322eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (𝑥𝑢) → (𝑋 = 𝑐𝑋 = (𝑥𝑢)))
24 pweq 4613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = (𝑥𝑢) → 𝒫 𝑐 = 𝒫 (𝑥𝑢))
2524ineq1d 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (𝑥𝑢) → (𝒫 𝑐 ∩ Fin) = (𝒫 (𝑥𝑢) ∩ Fin))
2625rexeqdv 3326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (𝑥𝑢) → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 ↔ ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑))
2723, 26imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (𝑥𝑢) → ((𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ↔ (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑)))
2827rspccv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → ((𝑥𝑢) ∈ 𝒫 𝑥 → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑)))
2921, 28mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑))
30 inss2 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝑢) ⊆ 𝑢
31 sstr 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑑 ⊆ (𝑥𝑢) ∧ (𝑥𝑢) ⊆ 𝑢) → 𝑑𝑢)
3230, 31mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 ⊆ (𝑥𝑢) → 𝑑𝑢)
3332anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑑 ⊆ (𝑥𝑢) ∧ 𝑑 ∈ Fin) → (𝑑𝑢𝑑 ∈ Fin))
34 elfpw 9395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) ↔ (𝑑 ⊆ (𝑥𝑢) ∧ 𝑑 ∈ Fin))
35 elfpw 9395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ↔ (𝑑𝑢𝑑 ∈ Fin))
3633, 34, 353imtr4i 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) → 𝑑 ∈ (𝒫 𝑢 ∩ Fin))
3736anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = 𝑑))
3837reximi2 3078 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑑 ∈ (𝒫 (𝑥𝑢) ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑)
3929, 38syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑))
40 unieq 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 𝑑 = 𝑏)
4140eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = 𝑏 → (𝑋 = 𝑑𝑋 = 𝑏))
4241cbvrexvw 3237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑑 ↔ ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
4339, 42imbitrdi 251 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
44 dfrex2 3072 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
4543, 44imbitrdi 251 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑋 = (𝑥𝑢) → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
4645con2d 134 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢)))
4746a1d 25 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ¬ 𝑋 = (𝑥𝑢))))
48473ad2ant2 1134 . . . . . . . . . . . . . . . . . . . 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 4915 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑢) ⊆ 𝑥
53 fiuni 9469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
5453elv 3484 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 = (fi‘𝑥)
55 fibas 22985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (fi‘𝑥) ∈ TopBases
56 unitg 22975 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘(fi‘𝑥)) = (fi‘𝑥)
5854, 57eqtr4i 2767 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 = (topGen‘(fi‘𝑥))
59 unieq 4917 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6058, 59eqtr4id 2795 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝑥 = 𝐽)
6160, 2eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 = (topGen‘(fi‘𝑥)) → 𝑥 = 𝑋)
62613ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝑥 = 𝑋)
6362adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → 𝑥 = 𝑋)
6452, 63sseqtrid 4025 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑥𝑢) ⊆ 𝑋)
65 eqcom 2743 . . . . . . . . . . . . . . . . . . 19 (𝑋 = (𝑥𝑢) ↔ (𝑥𝑢) = 𝑋)
66 eqss 3998 . . . . . . . . . . . . . . . . . . . 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 3989 . . . . . . . . . . . . . . . . 17 (𝑋 𝑢 → ( 𝑢 (𝑥𝑢) → 𝑋 (𝑥𝑢)))
7271con3rr3 155 . . . . . . . . . . . . . . . 16 𝑋 (𝑥𝑢) → (𝑋 𝑢 → ¬ 𝑢 (𝑥𝑢)))
7370, 72syl 17 . . . . . . . . . . . . . . 15 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑋 𝑢 → ¬ 𝑢 (𝑥𝑢)))
74 nss 4047 . . . . . . . . . . . . . . . . 17 𝑢 (𝑥𝑢) ↔ ∃𝑦(𝑦 𝑢 ∧ ¬ 𝑦 (𝑥𝑢)))
75 df-rex 3070 . . . . . . . . . . . . . . . . 17 (∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢) ↔ ∃𝑦(𝑦 𝑢 ∧ ¬ 𝑦 (𝑥𝑢)))
7674, 75bitr4i 278 . . . . . . . . . . . . . . . 16 𝑢 (𝑥𝑢) ↔ ∃𝑦 𝑢 ¬ 𝑦 (𝑥𝑢))
77 eluni2 4910 . . . . . . . . . . . . . . . . . 18 (𝑦 𝑢 ↔ ∃𝑤𝑢 𝑦𝑤)
78 elpwi 4606 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
7978sseld 3981 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑤𝑢𝑤 ∈ (fi‘𝑥)))
8079ad2antrl 728 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢𝑤 ∈ (fi‘𝑥)))
81 elfi 9454 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 ∈ V ∧ 𝑥 ∈ V) → (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡))
8281el2v 3486 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡)
8380, 82imbitrdi 251 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = 𝑡))
842alexsubALTlem3 24058 . . . . . . . . . . . . . . . . . . . . . . . . 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 9460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ V → 𝑥 ⊆ (fi‘𝑥))
8887elv 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑥 ⊆ (fi‘𝑥)
89 elinel1 4200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
9089elpwid 4608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
9190ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → 𝑡𝑥)
9291ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑡𝑥)
93 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠𝑡)
9492, 93sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠𝑥)
9588, 94sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑠 ∈ (fi‘𝑥))
9695snssd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → {𝑠} ⊆ (fi‘𝑥))
9786, 96unssd 4191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
98 fvex 6918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (fi‘𝑥) ∈ V
9998elpw2 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ↔ (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
10097, 99sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥))
101 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)) → 𝑎𝑢)
102101ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑎𝑢)
103 ssun1 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑢 ⊆ (𝑢 ∪ {𝑠})
104102, 103sstrdi 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑎 ⊆ (𝑢 ∪ {𝑠}))
105 unieq 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑏 𝑛 = 𝑏)
106105eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑏 → (𝑋 = 𝑛𝑋 = 𝑏))
107106notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑏 → (¬ 𝑋 = 𝑛 ↔ ¬ 𝑋 = 𝑏))
108107cbvralvw 3236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑢 ∪ {𝑠}) → (𝑎𝑧𝑎 ⊆ (𝑢 ∪ {𝑠})))
113 pweq 4613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑢 ∪ {𝑠}) → 𝒫 𝑧 = 𝒫 (𝑢 ∪ {𝑠}))
114113ineq1d 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑢 ∪ {𝑠}) → (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin))
115114raleqdv 3325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑢 ∪ {𝑠}) → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏))
116112, 115anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = (𝑢 ∪ {𝑠}) → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
117116elrab 3691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ↔ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑏)))
118111, 117sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)})
119 elun1 4181 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
121 vsnid 4662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ {𝑠}
122 elun2 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ {𝑠} → 𝑠 ∈ (𝑢 ∪ {𝑠}))
123121, 122ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑠 ∈ (𝑢 ∪ {𝑠})
124 intss1 4962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑠𝑡 𝑡𝑠)
125 sseq1 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑦𝑤)
133131, 132sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑠𝑡)
137135, 136sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑦𝑤) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))) → 𝑠𝑥)
138 elin 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ (𝑥𝑢) ↔ (𝑠𝑥𝑠𝑢))
139 elunii 4911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ V
150 eleq1w 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 → (𝑣 ∈ (𝑢 ∪ {𝑠}) ↔ 𝑠 ∈ (𝑢 ∪ {𝑠})))
151 elequ1 2114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 ↔ ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣𝑢))
157155, 156sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → ¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢)
158 eqimss2 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = (𝑢 ∪ {𝑠}) → (𝑢 ∪ {𝑠}) ⊆ 𝑢)
159158necon3bi 2966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ⊊ (𝑢 ∪ {𝑠}) ↔ (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
163161, 162sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) ∧ (𝑠𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)) → 𝑢 ⊊ (𝑢 ∪ {𝑠}))
164 psseq2 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3160 . . . . . . . . . . . . . . . . . . . . . . . 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 3152 . . . . . . . . . . . . . . . . . . . . 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 3152 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (∃𝑤𝑢 𝑦𝑤 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))
17477, 173biimtrid 242 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑦 𝑢 → (¬ 𝑦 (𝑥𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})𝑢𝑣)))
175174rexlimdv 3152 . . . . . . . . . . . . . . . 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 4177 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅})
183 eqimss2 4042 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎𝑎𝑧)
184183biantrurd 532 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)))
185 pweq 4613 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎)
186185ineq1d 4218 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑎 ∩ Fin))
187186raleqdv 3325 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
188184, 187bitr3d 281 . . . . . . . . . . . . . . 15 (𝑧 = 𝑎 → ((𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏))
189 simpll3 1214 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ 𝒫 (fi‘𝑥))
190 simplr 768 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏)
191188, 189, 190elrabd 3693 . . . . . . . . . . . . . 14 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)})
192182, 191sselid 3980 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = 𝑏)} ∪ {∅}))
193 psseq2 4090 . . . . . . . . . . . . . . 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 5355 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑎
199 0fi 9083 . . . . . . . . . . . . . . . . . 18 ∅ ∈ Fin
200198, 199elini 4198 . . . . . . . . . . . . . . . . 17 ∅ ∈ (𝒫 𝑎 ∩ Fin)
201197, 200eqeltrdi 2848 . . . . . . . . . . . . . . . 16 (𝑎 = ∅ → 𝑎 ∈ (𝒫 𝑎 ∩ Fin))
202 unieq 4917 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑎 𝑏 = 𝑎)
203202eqeq2d 2747 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑎 → (𝑋 = 𝑏𝑋 = 𝑎))
204203notbid 318 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑎 → (¬ 𝑋 = 𝑏 ↔ ¬ 𝑋 = 𝑎))
205204rspccv 3618 . . . . . . . . . . . . . . . 16 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑎 ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = 𝑎))
206201, 205syl5 34 . . . . . . . . . . . . . . 15 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑎 = ∅ → ¬ 𝑋 = 𝑎))
207206necon2ad 2954 . . . . . . . . . . . . . 14 (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑋 = 𝑎𝑎 ≠ ∅))
208207ad2antlr 727 . . . . . . . . . . . . 13 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑋 = 𝑎𝑎 ≠ ∅))
209 psseq1 4089 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢𝑎 ↔ ∅ ⊊ 𝑎))
210209adantl 481 . . . . . . . . . . . . . 14 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = 𝑏) ∧ 𝑢 = ∅) → (𝑢𝑎 ↔ ∅ ⊊ 𝑎))
211 0pss 4446 . . . . . . . . . . . . . 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 3152 . . . . . . 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 1119 . 2 (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) → (𝑎 ∈ 𝒫 (fi‘𝑥) → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
224223ralrimdv 3151 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 1539  wex 1778  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  Vcvv 3479  cun 3948  cin 3949  wss 3950  wpss 3951  c0 4332  𝒫 cpw 4599  {csn 4625   cuni 4906   cint 4945  cfv 6560  Fincfn 8986  ficfi 9451  topGenctg 17483  TopBasesctb 22953
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-ac2 10504
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-rpss 7744  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-1o 8507  df-2o 8508  df-en 8987  df-fin 8990  df-fi 9452  df-card 9980  df-ac 10157  df-topgen 17489  df-bases 22954
This theorem is referenced by:  alexsubALT  24060
  Copyright terms: Public domain W3C validator