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

Theorem alexsubALTlem4 23417
Description: Lemma for alexsubALT 23418. 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 3076 . . . . 5 (βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 ↔ Β¬ βˆƒπ‘ ∈ (𝒫 π‘Ž ∩ Fin)𝑋 = βˆͺ 𝑏)
2 alexsubALT.1 . . . . . . . 8 𝑋 = βˆͺ 𝐽
32alexsubALTlem2 23415 . . . . . . 7 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ βˆƒπ‘’ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣)
4 elun 4113 . . . . . . . . . 10 (𝑒 ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) ↔ (𝑒 ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} ∨ 𝑒 ∈ {βˆ…}))
5 sseq2 3975 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ (π‘Ž βŠ† 𝑧 ↔ π‘Ž βŠ† 𝑒))
6 pweq 4579 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ 𝒫 𝑧 = 𝒫 𝑒)
76ineq1d 4176 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ (𝒫 𝑧 ∩ Fin) = (𝒫 𝑒 ∩ Fin))
87raleqdv 3316 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ (βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 ↔ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))
95, 8anbi12d 632 . . . . . . . . . . . 12 (𝑧 = 𝑒 β†’ ((π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ↔ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)))
109elrab 3650 . . . . . . . . . . 11 (𝑒 ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} ↔ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)))
11 velsn 4607 . . . . . . . . . . 11 (𝑒 ∈ {βˆ…} ↔ 𝑒 = βˆ…)
1210, 11orbi12i 914 . . . . . . . . . 10 ((𝑒 ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} ∨ 𝑒 ∈ {βˆ…}) ↔ ((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) ∨ 𝑒 = βˆ…))
134, 12bitri 275 . . . . . . . . 9 (𝑒 ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) ↔ ((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) ∨ 𝑒 = βˆ…))
14 ralnex 3076 . . . . . . . . . . . . 13 (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)
15 simprrl 780 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ π‘Ž βŠ† 𝑒)
1615unissd 4880 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ βˆͺ π‘Ž βŠ† βˆͺ 𝑒)
17 sseq1 3974 . . . . . . . . . . . . . . . 16 (𝑋 = βˆͺ π‘Ž β†’ (𝑋 βŠ† βˆͺ 𝑒 ↔ βˆͺ π‘Ž βŠ† βˆͺ 𝑒))
1816, 17syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑋 = βˆͺ π‘Ž β†’ 𝑋 βŠ† βˆͺ 𝑒))
19 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 π‘₯ ∈ V
20 inss1 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∩ 𝑒) βŠ† π‘₯
2119, 20elpwi2 5308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ ∩ 𝑒) ∈ 𝒫 π‘₯
22 unieq 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (π‘₯ ∩ 𝑒) β†’ βˆͺ 𝑐 = βˆͺ (π‘₯ ∩ 𝑒))
2322eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (π‘₯ ∩ 𝑒) β†’ (𝑋 = βˆͺ 𝑐 ↔ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒)))
24 pweq 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = (π‘₯ ∩ 𝑒) β†’ 𝒫 𝑐 = 𝒫 (π‘₯ ∩ 𝑒))
2524ineq1d 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = (π‘₯ ∩ 𝑒) β†’ (𝒫 𝑐 ∩ Fin) = (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin))
2625rexeqdv 3317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (π‘₯ ∩ 𝑒) β†’ (βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑 ↔ βˆƒπ‘‘ ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin)𝑋 = βˆͺ 𝑑))
2723, 26imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (π‘₯ ∩ 𝑒) β†’ ((𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ↔ (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘‘ ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin)𝑋 = βˆͺ 𝑑)))
2827rspccv 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ ((π‘₯ ∩ 𝑒) ∈ 𝒫 π‘₯ β†’ (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘‘ ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin)𝑋 = βˆͺ 𝑑)))
2921, 28mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘‘ ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin)𝑋 = βˆͺ 𝑑))
30 inss2 4194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘₯ ∩ 𝑒) βŠ† 𝑒
31 sstr 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑑 βŠ† (π‘₯ ∩ 𝑒) ∧ (π‘₯ ∩ 𝑒) βŠ† 𝑒) β†’ 𝑑 βŠ† 𝑒)
3230, 31mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 βŠ† (π‘₯ ∩ 𝑒) β†’ 𝑑 βŠ† 𝑒)
3332anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑑 βŠ† (π‘₯ ∩ 𝑒) ∧ 𝑑 ∈ Fin) β†’ (𝑑 βŠ† 𝑒 ∧ 𝑑 ∈ Fin))
34 elfpw 9305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin) ↔ (𝑑 βŠ† (π‘₯ ∩ 𝑒) ∧ 𝑑 ∈ Fin))
35 elfpw 9305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 ∈ (𝒫 𝑒 ∩ Fin) ↔ (𝑑 βŠ† 𝑒 ∧ 𝑑 ∈ Fin))
3633, 34, 353imtr4i 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin) β†’ 𝑑 ∈ (𝒫 𝑒 ∩ Fin))
3736anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑑 ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑑) β†’ (𝑑 ∈ (𝒫 𝑒 ∩ Fin) ∧ 𝑋 = βˆͺ 𝑑))
3837reximi2 3083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒπ‘‘ ∈ (𝒫 (π‘₯ ∩ 𝑒) ∩ Fin)𝑋 = βˆͺ 𝑑 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑑)
3929, 38syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘‘ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑑))
40 unieq 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 β†’ βˆͺ 𝑑 = βˆͺ 𝑏)
4140eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = 𝑏 β†’ (𝑋 = βˆͺ 𝑑 ↔ 𝑋 = βˆͺ 𝑏))
4241cbvrexvw 3229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆƒπ‘‘ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑑 ↔ βˆƒπ‘ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑏)
4339, 42syl6ib 251 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑏))
44 dfrex2 3077 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑏 ↔ Β¬ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)
4543, 44syl6ib 251 . . . . . . . . . . . . . . . . . . . . . . 23 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) β†’ Β¬ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))
4645con2d 134 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ Β¬ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒)))
4746a1d 25 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (π‘Ž βŠ† 𝑒 β†’ (βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ Β¬ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒))))
48473ad2ant2 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) β†’ (π‘Ž βŠ† 𝑒 β†’ (βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ Β¬ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒))))
4948adantr 482 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ 𝑒 ∈ 𝒫 (fiβ€˜π‘₯)) β†’ (π‘Ž βŠ† 𝑒 β†’ (βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ Β¬ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒))))
5049impd 412 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ 𝑒 ∈ 𝒫 (fiβ€˜π‘₯)) β†’ ((π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ Β¬ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒)))
5150impr 456 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ Β¬ 𝑋 = βˆͺ (π‘₯ ∩ 𝑒))
5220unissi 4879 . . . . . . . . . . . . . . . . . . 19 βˆͺ (π‘₯ ∩ 𝑒) βŠ† βˆͺ π‘₯
53 fiuni 9371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ V β†’ βˆͺ π‘₯ = βˆͺ (fiβ€˜π‘₯))
5453elv 3454 . . . . . . . . . . . . . . . . . . . . . . . 24 βˆͺ π‘₯ = βˆͺ (fiβ€˜π‘₯)
55 fibas 22343 . . . . . . . . . . . . . . . . . . . . . . . . 25 (fiβ€˜π‘₯) ∈ TopBases
56 unitg 22333 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((fiβ€˜π‘₯) ∈ TopBases β†’ βˆͺ (topGenβ€˜(fiβ€˜π‘₯)) = βˆͺ (fiβ€˜π‘₯))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 βˆͺ (topGenβ€˜(fiβ€˜π‘₯)) = βˆͺ (fiβ€˜π‘₯)
5854, 57eqtr4i 2768 . . . . . . . . . . . . . . . . . . . . . . 23 βˆͺ π‘₯ = βˆͺ (topGenβ€˜(fiβ€˜π‘₯))
59 unieq 4881 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) β†’ βˆͺ 𝐽 = βˆͺ (topGenβ€˜(fiβ€˜π‘₯)))
6058, 59eqtr4id 2796 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) β†’ βˆͺ π‘₯ = βˆͺ 𝐽)
6160, 2eqtr4di 2795 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) β†’ βˆͺ π‘₯ = 𝑋)
62613ad2ant1 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) β†’ βˆͺ π‘₯ = 𝑋)
6362adantr 482 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ βˆͺ π‘₯ = 𝑋)
6452, 63sseqtrid 4001 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ βˆͺ (π‘₯ ∩ 𝑒) βŠ† 𝑋)
65 eqcom 2744 . . . . . . . . . . . . . . . . . . 19 (𝑋 = βˆͺ (π‘₯ ∩ 𝑒) ↔ βˆͺ (π‘₯ ∩ 𝑒) = 𝑋)
66 eqss 3964 . . . . . . . . . . . . . . . . . . . 20 (βˆͺ (π‘₯ ∩ 𝑒) = 𝑋 ↔ (βˆͺ (π‘₯ ∩ 𝑒) βŠ† 𝑋 ∧ 𝑋 βŠ† βˆͺ (π‘₯ ∩ 𝑒)))
6766baib 537 . . . . . . . . . . . . . . . . . . 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 3956 . . . . . . . . . . . . . . . . 17 (𝑋 βŠ† βˆͺ 𝑒 β†’ (βˆͺ 𝑒 βŠ† βˆͺ (π‘₯ ∩ 𝑒) β†’ 𝑋 βŠ† βˆͺ (π‘₯ ∩ 𝑒)))
7271con3rr3 155 . . . . . . . . . . . . . . . 16 (Β¬ 𝑋 βŠ† βˆͺ (π‘₯ ∩ 𝑒) β†’ (𝑋 βŠ† βˆͺ 𝑒 β†’ Β¬ βˆͺ 𝑒 βŠ† βˆͺ (π‘₯ ∩ 𝑒)))
7370, 72syl 17 . . . . . . . . . . . . . . 15 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑋 βŠ† βˆͺ 𝑒 β†’ Β¬ βˆͺ 𝑒 βŠ† βˆͺ (π‘₯ ∩ 𝑒)))
74 nss 4011 . . . . . . . . . . . . . . . . 17 (Β¬ βˆͺ 𝑒 βŠ† βˆͺ (π‘₯ ∩ 𝑒) ↔ βˆƒπ‘¦(𝑦 ∈ βˆͺ 𝑒 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))
75 df-rex 3075 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘¦ ∈ βˆͺ 𝑒 Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) ↔ βˆƒπ‘¦(𝑦 ∈ βˆͺ 𝑒 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))
7674, 75bitr4i 278 . . . . . . . . . . . . . . . 16 (Β¬ βˆͺ 𝑒 βŠ† βˆͺ (π‘₯ ∩ 𝑒) ↔ βˆƒπ‘¦ ∈ βˆͺ 𝑒 Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒))
77 eluni2 4874 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ βˆͺ 𝑒 ↔ βˆƒπ‘€ ∈ 𝑒 𝑦 ∈ 𝑀)
78 elpwi 4572 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) β†’ 𝑒 βŠ† (fiβ€˜π‘₯))
7978sseld 3948 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) β†’ (𝑀 ∈ 𝑒 β†’ 𝑀 ∈ (fiβ€˜π‘₯)))
8079ad2antrl 727 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑀 ∈ 𝑒 β†’ 𝑀 ∈ (fiβ€˜π‘₯)))
81 elfi 9356 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ V ∧ π‘₯ ∈ V) β†’ (𝑀 ∈ (fiβ€˜π‘₯) ↔ βˆƒπ‘‘ ∈ (𝒫 π‘₯ ∩ Fin)𝑀 = ∩ 𝑑))
8281el2v 3456 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (fiβ€˜π‘₯) ↔ βˆƒπ‘‘ ∈ (𝒫 π‘₯ ∩ Fin)𝑀 = ∩ 𝑑)
8380, 82syl6ib 251 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑀 ∈ 𝑒 β†’ βˆƒπ‘‘ ∈ (𝒫 π‘₯ ∩ Fin)𝑀 = ∩ 𝑑))
842alexsubALTlem3 23416 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) β†’ βˆƒπ‘  ∈ 𝑑 βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)
8578adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) β†’ 𝑒 βŠ† (fiβ€˜π‘₯))
8685ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑒 βŠ† (fiβ€˜π‘₯))
87 ssfii 9362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (π‘₯ ∈ V β†’ π‘₯ βŠ† (fiβ€˜π‘₯))
8887elv 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 π‘₯ βŠ† (fiβ€˜π‘₯)
89 elinel1 4160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑑 ∈ (𝒫 π‘₯ ∩ Fin) β†’ 𝑑 ∈ 𝒫 π‘₯)
9089elpwid 4574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑑 ∈ (𝒫 π‘₯ ∩ Fin) β†’ 𝑑 βŠ† π‘₯)
9190ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒))) β†’ 𝑑 βŠ† π‘₯)
9291ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑑 βŠ† π‘₯)
93 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑠 ∈ 𝑑)
9492, 93sseldd 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑠 ∈ π‘₯)
9588, 94sselid 3947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑠 ∈ (fiβ€˜π‘₯))
9695snssd 4774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ {𝑠} βŠ† (fiβ€˜π‘₯))
9786, 96unssd 4151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ (𝑒 βˆͺ {𝑠}) βŠ† (fiβ€˜π‘₯))
98 fvex 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (fiβ€˜π‘₯) ∈ V
9998elpw2 5307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑒 βˆͺ {𝑠}) ∈ 𝒫 (fiβ€˜π‘₯) ↔ (𝑒 βˆͺ {𝑠}) βŠ† (fiβ€˜π‘₯))
10097, 99sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ (𝑒 βˆͺ {𝑠}) ∈ 𝒫 (fiβ€˜π‘₯))
101 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) β†’ π‘Ž βŠ† 𝑒)
102101ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ π‘Ž βŠ† 𝑒)
103 ssun1 4137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑒 βŠ† (𝑒 βˆͺ {𝑠})
104102, 103sstrdi 3961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ π‘Ž βŠ† (𝑒 βˆͺ {𝑠}))
105 unieq 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑏 β†’ βˆͺ 𝑛 = βˆͺ 𝑏)
106105eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑏 β†’ (𝑋 = βˆͺ 𝑛 ↔ 𝑋 = βˆͺ 𝑏))
107106notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑏 β†’ (Β¬ 𝑋 = βˆͺ 𝑛 ↔ Β¬ 𝑋 = βˆͺ 𝑏))
108107cbvralvw 3228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛 ↔ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)
109108biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛 β†’ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)
110109ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)
111100, 104, 110jca32 517 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ ((𝑒 βˆͺ {𝑠}) ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† (𝑒 βˆͺ {𝑠}) ∧ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)))
112 sseq2 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑒 βˆͺ {𝑠}) β†’ (π‘Ž βŠ† 𝑧 ↔ π‘Ž βŠ† (𝑒 βˆͺ {𝑠})))
113 pweq 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑒 βˆͺ {𝑠}) β†’ 𝒫 𝑧 = 𝒫 (𝑒 βˆͺ {𝑠}))
114113ineq1d 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑒 βˆͺ {𝑠}) β†’ (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin))
115114raleqdv 3316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑒 βˆͺ {𝑠}) β†’ (βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 ↔ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))
116112, 115anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = (𝑒 βˆͺ {𝑠}) β†’ ((π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ↔ (π‘Ž βŠ† (𝑒 βˆͺ {𝑠}) ∧ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)))
117116elrab 3650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑒 βˆͺ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} ↔ ((𝑒 βˆͺ {𝑠}) ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† (𝑒 βˆͺ {𝑠}) ∧ βˆ€π‘ ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)))
118111, 117sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ (𝑒 βˆͺ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)})
119 elun1 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑒 βˆͺ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} β†’ (𝑒 βˆͺ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}))
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ (𝑒 βˆͺ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}))
121 vsnid 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ {𝑠}
122 elun2 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ {𝑠} β†’ 𝑠 ∈ (𝑒 βˆͺ {𝑠}))
123121, 122ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑠 ∈ (𝑒 βˆͺ {𝑠})
124 intss1 4929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑠 ∈ 𝑑 β†’ ∩ 𝑑 βŠ† 𝑠)
125 sseq1 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 = ∩ 𝑑 β†’ (𝑀 βŠ† 𝑠 ↔ ∩ 𝑑 βŠ† 𝑠))
126124, 125syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑠 ∈ 𝑑 β†’ (𝑀 = ∩ 𝑑 β†’ 𝑀 βŠ† 𝑠))
127126impcom 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑀 = ∩ 𝑑 ∧ 𝑠 ∈ 𝑑) β†’ 𝑀 βŠ† 𝑠)
128127ad4ant24 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ 𝑠 ∈ 𝑑) β†’ 𝑀 βŠ† 𝑠)
129128adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 ∈ 𝑒 ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ 𝑠 ∈ 𝑑)) β†’ 𝑀 βŠ† 𝑠)
130129adantrrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑀 ∈ 𝑒 ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑀 βŠ† 𝑠)
131130adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑀 βŠ† 𝑠)
132 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑦 ∈ 𝑀)
133131, 132sseldd 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑦 ∈ 𝑠)
13490ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) β†’ 𝑑 βŠ† π‘₯)
135134ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑑 βŠ† π‘₯)
136 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑠 ∈ 𝑑)
137135, 136sseldd 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ (((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛))) β†’ 𝑠 ∈ π‘₯)
138 elin 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ (π‘₯ ∩ 𝑒) ↔ (𝑠 ∈ π‘₯ ∧ 𝑠 ∈ 𝑒))
139 elunii 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ (π‘₯ ∩ 𝑒)) β†’ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒))
140139ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ 𝑠 β†’ (𝑠 ∈ (π‘₯ ∩ 𝑒) β†’ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))
141138, 140biimtrrid 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ 𝑠 β†’ ((𝑠 ∈ π‘₯ ∧ 𝑠 ∈ 𝑒) β†’ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))
142141expd 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀)) β†’ ((𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛) β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ Β¬ 𝑠 ∈ 𝑒)))
146145com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ 𝑦 ∈ 𝑀)) β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ ((𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛) β†’ Β¬ 𝑠 ∈ 𝑒)))
147146exp32 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) β†’ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) β†’ (𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ ((𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛) β†’ Β¬ 𝑠 ∈ 𝑒)))))
148147imp55 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ Β¬ 𝑠 ∈ 𝑒)
149 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑠 ∈ V
150 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 β†’ (𝑣 ∈ (𝑒 βˆͺ {𝑠}) ↔ 𝑠 ∈ (𝑒 βˆͺ {𝑠})))
151 elequ1 2114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = 𝑠 β†’ (𝑣 ∈ 𝑒 ↔ 𝑠 ∈ 𝑒))
152151notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑠 β†’ (Β¬ 𝑣 ∈ 𝑒 ↔ Β¬ 𝑠 ∈ 𝑒))
153150, 152anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = 𝑠 β†’ ((𝑣 ∈ (𝑒 βˆͺ {𝑠}) ∧ Β¬ 𝑣 ∈ 𝑒) ↔ (𝑠 ∈ (𝑒 βˆͺ {𝑠}) ∧ Β¬ 𝑠 ∈ 𝑒)))
154149, 153spcev 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝑒 βˆͺ {𝑠}) ∧ Β¬ 𝑠 ∈ 𝑒) β†’ βˆƒπ‘£(𝑣 ∈ (𝑒 βˆͺ {𝑠}) ∧ Β¬ 𝑣 ∈ 𝑒))
155123, 148, 154sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ βˆƒπ‘£(𝑣 ∈ (𝑒 βˆͺ {𝑠}) ∧ Β¬ 𝑣 ∈ 𝑒))
156 nss 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Β¬ (𝑒 βˆͺ {𝑠}) βŠ† 𝑒 ↔ βˆƒπ‘£(𝑣 ∈ (𝑒 βˆͺ {𝑠}) ∧ Β¬ 𝑣 ∈ 𝑒))
157155, 156sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ Β¬ (𝑒 βˆͺ {𝑠}) βŠ† 𝑒)
158 eqimss2 4006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑒 = (𝑒 βˆͺ {𝑠}) β†’ (𝑒 βˆͺ {𝑠}) βŠ† 𝑒)
159158necon3bi 2971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Β¬ (𝑒 βˆͺ {𝑠}) βŠ† 𝑒 β†’ 𝑒 β‰  (𝑒 βˆͺ {𝑠}))
160157, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑒 β‰  (𝑒 βˆͺ {𝑠}))
161160, 103jctil 521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ (𝑒 βŠ† (𝑒 βˆͺ {𝑠}) ∧ 𝑒 β‰  (𝑒 βˆͺ {𝑠})))
162 df-pss 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 ⊊ (𝑒 βˆͺ {𝑠}) ↔ (𝑒 βŠ† (𝑒 βˆͺ {𝑠}) ∧ 𝑒 β‰  (𝑒 βˆͺ {𝑠})))
163161, 162sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ 𝑒 ⊊ (𝑒 βˆͺ {𝑠}))
164 psseq2 4053 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = (𝑒 βˆͺ {𝑠}) β†’ (𝑒 ⊊ 𝑣 ↔ 𝑒 ⊊ (𝑒 βˆͺ {𝑠})))
165164rspcev 3584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑒 βˆͺ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) ∧ 𝑒 ⊊ (𝑒 βˆͺ {𝑠})) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)
166120, 163, 165syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) ∧ (𝑠 ∈ 𝑑 ∧ βˆ€π‘› ∈ (𝒫 (𝑒 βˆͺ {𝑠}) ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑛)) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)
16784, 166rexlimddv 3159 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) ∧ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) ∧ (𝑦 ∈ 𝑀 ∧ Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒)))) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)
168167exp45 440 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) β†’ ((𝑑 ∈ (𝒫 π‘₯ ∩ Fin) ∧ 𝑀 = ∩ 𝑑) β†’ (𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣))))
169168expd 417 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) β†’ (𝑑 ∈ (𝒫 π‘₯ ∩ Fin) β†’ (𝑀 = ∩ 𝑑 β†’ (𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)))))
170169rexlimdv 3151 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) ∧ 𝑀 ∈ 𝑒) β†’ (βˆƒπ‘‘ ∈ (𝒫 π‘₯ ∩ Fin)𝑀 = ∩ 𝑑 β†’ (𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣))))
171170ex 414 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑀 ∈ 𝑒 β†’ (βˆƒπ‘‘ ∈ (𝒫 π‘₯ ∩ Fin)𝑀 = ∩ 𝑑 β†’ (𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)))))
17283, 171mpdd 43 . . . . . . . . . . . . . . . . . . 19 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑀 ∈ 𝑒 β†’ (𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣))))
173172rexlimdv 3151 . . . . . . . . . . . . . . . . . 18 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (βˆƒπ‘€ ∈ 𝑒 𝑦 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)))
17477, 173biimtrid 241 . . . . . . . . . . . . . . . . 17 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (𝑦 ∈ βˆͺ 𝑒 β†’ (Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣)))
175174rexlimdv 3151 . . . . . . . . . . . . . . . 16 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (βˆƒπ‘¦ ∈ βˆͺ 𝑒 Β¬ 𝑦 ∈ βˆͺ (π‘₯ ∩ 𝑒) β†’ βˆƒπ‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})𝑒 ⊊ 𝑣))
17676, 175biimtrid 241 . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . 12 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ (𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž))
180179ex 414 . . . . . . . . . . 11 ((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) β†’ ((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž)))
181180adantr 482 . . . . . . . . . 10 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ ((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž)))
182 ssun1 4137 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βŠ† ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})
183 eqimss2 4006 . . . . . . . . . . . . . . . . 17 (𝑧 = π‘Ž β†’ π‘Ž βŠ† 𝑧)
184183biantrurd 534 . . . . . . . . . . . . . . . 16 (𝑧 = π‘Ž β†’ (βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 ↔ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)))
185 pweq 4579 . . . . . . . . . . . . . . . . . 18 (𝑧 = π‘Ž β†’ 𝒫 𝑧 = 𝒫 π‘Ž)
186185ineq1d 4176 . . . . . . . . . . . . . . . . 17 (𝑧 = π‘Ž β†’ (𝒫 𝑧 ∩ Fin) = (𝒫 π‘Ž ∩ Fin))
187186raleqdv 3316 . . . . . . . . . . . . . . . 16 (𝑧 = π‘Ž β†’ (βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 ↔ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))
188184, 187bitr3d 281 . . . . . . . . . . . . . . 15 (𝑧 = π‘Ž β†’ ((π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ↔ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏))
189 simpll3 1215 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯))
190 simplr 768 . . . . . . . . . . . . . . 15 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)
191188, 189, 190elrabd 3652 . . . . . . . . . . . . . 14 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ π‘Ž ∈ {𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)})
192182, 191sselid 3947 . . . . . . . . . . . . 13 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ π‘Ž ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}))
193 psseq2 4053 . . . . . . . . . . . . . . 15 (𝑣 = π‘Ž β†’ (𝑒 ⊊ 𝑣 ↔ 𝑒 ⊊ π‘Ž))
194193notbid 318 . . . . . . . . . . . . . 14 (𝑣 = π‘Ž β†’ (Β¬ 𝑒 ⊊ 𝑣 ↔ Β¬ 𝑒 ⊊ π‘Ž))
195194rspcv 3580 . . . . . . . . . . . . 13 (π‘Ž ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑒 ⊊ π‘Ž))
196192, 195syl 17 . . . . . . . . . . . 12 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑒 ⊊ π‘Ž))
197 id 22 . . . . . . . . . . . . . . . . 17 (π‘Ž = βˆ… β†’ π‘Ž = βˆ…)
198 0elpw 5316 . . . . . . . . . . . . . . . . . 18 βˆ… ∈ 𝒫 π‘Ž
199 0fin 9122 . . . . . . . . . . . . . . . . . 18 βˆ… ∈ Fin
200198, 199elini 4158 . . . . . . . . . . . . . . . . 17 βˆ… ∈ (𝒫 π‘Ž ∩ Fin)
201197, 200eqeltrdi 2846 . . . . . . . . . . . . . . . 16 (π‘Ž = βˆ… β†’ π‘Ž ∈ (𝒫 π‘Ž ∩ Fin))
202 unieq 4881 . . . . . . . . . . . . . . . . . . 19 (𝑏 = π‘Ž β†’ βˆͺ 𝑏 = βˆͺ π‘Ž)
203202eqeq2d 2748 . . . . . . . . . . . . . . . . . 18 (𝑏 = π‘Ž β†’ (𝑋 = βˆͺ 𝑏 ↔ 𝑋 = βˆͺ π‘Ž))
204203notbid 318 . . . . . . . . . . . . . . . . 17 (𝑏 = π‘Ž β†’ (Β¬ 𝑋 = βˆͺ 𝑏 ↔ Β¬ 𝑋 = βˆͺ π‘Ž))
205204rspccv 3581 . . . . . . . . . . . . . . . 16 (βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ (π‘Ž ∈ (𝒫 π‘Ž ∩ Fin) β†’ Β¬ 𝑋 = βˆͺ π‘Ž))
206201, 205syl5 34 . . . . . . . . . . . . . . 15 (βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ (π‘Ž = βˆ… β†’ Β¬ 𝑋 = βˆͺ π‘Ž))
207206necon2ad 2959 . . . . . . . . . . . . . 14 (βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ (𝑋 = βˆͺ π‘Ž β†’ π‘Ž β‰  βˆ…))
208207ad2antlr 726 . . . . . . . . . . . . 13 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ (𝑋 = βˆͺ π‘Ž β†’ π‘Ž β‰  βˆ…))
209 psseq1 4052 . . . . . . . . . . . . . . 15 (𝑒 = βˆ… β†’ (𝑒 ⊊ π‘Ž ↔ βˆ… ⊊ π‘Ž))
210209adantl 483 . . . . . . . . . . . . . 14 ((((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) ∧ 𝑒 = βˆ…) β†’ (𝑒 ⊊ π‘Ž ↔ βˆ… ⊊ π‘Ž))
211 0pss 4409 . . . . . . . . . . . . . 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 414 . . . . . . . . . 10 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ (𝑒 = βˆ… β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž)))
216181, 215jaod 858 . . . . . . . . 9 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ (((𝑒 ∈ 𝒫 (fiβ€˜π‘₯) ∧ (π‘Ž βŠ† 𝑒 ∧ βˆ€π‘ ∈ (𝒫 𝑒 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)) ∨ 𝑒 = βˆ…) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž)))
21713, 216biimtrid 241 . . . . . . . 8 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ (𝑒 ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) β†’ (βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž)))
218217rexlimdv 3151 . . . . . . 7 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ (βˆƒπ‘’ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…})βˆ€π‘£ ∈ ({𝑧 ∈ 𝒫 (fiβ€˜π‘₯) ∣ (π‘Ž βŠ† 𝑧 ∧ βˆ€π‘ ∈ (𝒫 𝑧 ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏)} βˆͺ {βˆ…}) Β¬ 𝑒 ⊊ 𝑣 β†’ Β¬ 𝑋 = βˆͺ π‘Ž))
2193, 218mpd 15 . . . . . 6 (((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏) β†’ Β¬ 𝑋 = βˆͺ π‘Ž)
220219ex 414 . . . . 5 ((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) β†’ (βˆ€π‘ ∈ (𝒫 π‘Ž ∩ Fin) Β¬ 𝑋 = βˆͺ 𝑏 β†’ Β¬ 𝑋 = βˆͺ π‘Ž))
2211, 220biimtrrid 242 . . . 4 ((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) β†’ (Β¬ βˆƒπ‘ ∈ (𝒫 π‘Ž ∩ Fin)𝑋 = βˆͺ 𝑏 β†’ Β¬ 𝑋 = βˆͺ π‘Ž))
222221con4d 115 . . 3 ((𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) ∧ π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)) β†’ (𝑋 = βˆͺ π‘Ž β†’ βˆƒπ‘ ∈ (𝒫 π‘Ž ∩ Fin)𝑋 = βˆͺ 𝑏))
2232223exp 1120 . 2 (𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) β†’ (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ (π‘Ž ∈ 𝒫 (fiβ€˜π‘₯) β†’ (𝑋 = βˆͺ π‘Ž β†’ βˆƒπ‘ ∈ (𝒫 π‘Ž ∩ Fin)𝑋 = βˆͺ 𝑏))))
224223ralrimdv 3150 1 (𝐽 = (topGenβ€˜(fiβ€˜π‘₯)) β†’ (βˆ€π‘ ∈ 𝒫 π‘₯(𝑋 = βˆͺ 𝑐 β†’ βˆƒπ‘‘ ∈ (𝒫 𝑐 ∩ Fin)𝑋 = βˆͺ 𝑑) β†’ βˆ€π‘Ž ∈ 𝒫 (fiβ€˜π‘₯)(𝑋 = βˆͺ π‘Ž β†’ βˆƒπ‘ ∈ (𝒫 π‘Ž ∩ Fin)𝑋 = βˆͺ 𝑏)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410  Vcvv 3448   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915   ⊊ wpss 3916  βˆ…c0 4287  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870  βˆ© cint 4912  β€˜cfv 6501  Fincfn 8890  ficfi 9353  topGenctg 17326  TopBasesctb 22311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-ac2 10406
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-rpss 7665  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-1o 8417  df-er 8655  df-en 8891  df-fin 8894  df-fi 9354  df-card 9882  df-ac 10059  df-topgen 17332  df-bases 22312
This theorem is referenced by:  alexsubALT  23418
  Copyright terms: Public domain W3C validator