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

Theorem alexsubALTlem3 22652
Description: Lemma for alexsubALT 22654. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
Hypothesis
Ref Expression
alexsubALT.1 𝑋 = 𝐽
Assertion
Ref Expression
alexsubALTlem3 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑛,𝑠,𝑡,𝑢,𝑤,𝑥,𝑦,𝐽   𝑋,𝑎,𝑏,𝑐,𝑑,𝑛,𝑠,𝑡,𝑢,𝑤,𝑥,𝑦

Proof of Theorem alexsubALTlem3
Dummy variables 𝑓 𝑚 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrex2 3227 . . . . . . . . . . 11 (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
21ralbii 3157 . . . . . . . . . 10 (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
3 ralnex 3224 . . . . . . . . . 10 (∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
42, 3bitr2i 279 . . . . . . . . 9 (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛)
5 elin 3924 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6 elpwi 4520 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
76adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8 uncom 4104 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
97, 8sseqtrdi 3992 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10 ssundif 4405 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
119, 10sylib 221 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12 diffi 8738 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
1312adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
1411, 13jca 515 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
155, 14sylbi 220 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1615adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1716ad2antll 728 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18 elin 3924 . . . . . . . . . . . . . . . . 17 ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19 vex 3472 . . . . . . . . . . . . . . . . . . 19 𝑢 ∈ V
2019elpw2 5224 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
2120anbi1i 626 . . . . . . . . . . . . . . . . 17 (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
2218, 21bitr2i 279 . . . . . . . . . . . . . . . 16 (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
2317, 22sylib 221 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24 simprrr 781 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = 𝑛)
25 eldif 3918 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
2625simplbi2 504 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27 elun 4100 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28 orcom 867 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
2927, 28bitr4i 281 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30 df-or 845 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
3129, 30bitr2i 279 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3226, 31sylib 221 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑛𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3332ssriv 3946 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34 uniss 4821 . . . . . . . . . . . . . . . . . . 19 (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3533, 34mp1i 13 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36 uniun 4836 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ {𝑠})
37 vex 3472 . . . . . . . . . . . . . . . . . . . . 21 𝑠 ∈ V
3837unisn 4833 . . . . . . . . . . . . . . . . . . . 20 {𝑠} = 𝑠
3938uneq2i 4111 . . . . . . . . . . . . . . . . . . 19 ( (𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4036, 39eqtri 2845 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4135, 40sseqtrdi 3992 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
4224, 41eqsstrd 3980 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
43 difss 4083 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∖ {𝑠}) ⊆ 𝑛
4443unissi 4822 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∖ {𝑠}) ⊆ 𝑛
45 sseq2 3968 . . . . . . . . . . . . . . . . . . . 20 (𝑋 = 𝑛 → ( (𝑛 ∖ {𝑠}) ⊆ 𝑋 (𝑛 ∖ {𝑠}) ⊆ 𝑛))
4644, 45mpbiri 261 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑛 (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4746adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4847ad2antll 728 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
49 elinel1 4146 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
5049elpwid 4522 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
5150ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) → 𝑡𝑥)
5251ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑡𝑥)
53 simprl 770 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑡)
5452, 53sseldd 3943 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑥)
55 elssuni 4843 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑥𝑠 𝑥)
5654, 55syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠 𝑥)
57 fibas 21580 . . . . . . . . . . . . . . . . . . . . 21 (fi‘𝑥) ∈ TopBases
58 unitg 21570 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
5957, 58mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
60 unieq 4824 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
61603ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6261ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝐽 = (topGen‘(fi‘𝑥)))
63 vex 3472 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
64 fiuni 8880 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
6563, 64mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = (fi‘𝑥))
6659, 62, 653eqtr4rd 2868 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝐽)
67 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19 𝑋 = 𝐽
6866, 67eqtr4di 2875 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝑋)
6956, 68sseqtrd 3982 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑋)
7048, 69unssd 4137 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ( (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
7142, 70eqssd 3959 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
72 unieq 4824 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 ∖ {𝑠}) → 𝑚 = (𝑛 ∖ {𝑠}))
7372uneq1d 4113 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑛 ∖ {𝑠}) → ( 𝑚𝑠) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
7473rspceeqv 3613 . . . . . . . . . . . . . . 15 (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7523, 71, 74syl2anc 587 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7675expr 460 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7776expd 419 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))))
7877rexlimdv 3269 . . . . . . . . . . 11 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7978ralimdva 3169 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
80 elinel2 4147 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
8180adantr 484 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → 𝑡 ∈ Fin)
82 unieq 4824 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑓𝑠) → 𝑚 = (𝑓𝑠))
8382uneq1d 4113 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑓𝑠) → ( 𝑚𝑠) = ( (𝑓𝑠) ∪ 𝑠))
8483eqeq2d 2833 . . . . . . . . . . . . . . 15 (𝑚 = (𝑓𝑠) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8584ac6sfi 8750 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8685ex 416 . . . . . . . . . . . . 13 (𝑡 ∈ Fin → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
8781, 86syl 17 . . . . . . . . . . . 12 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
8887adantr 484 . . . . . . . . . . 11 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
8988ad2antrl 727 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
90 ffvelrn 6831 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin))
91 elin 3924 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin))
92 elpwi 4520 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑠) ∈ 𝒫 𝑢 → (𝑓𝑠) ⊆ 𝑢)
9392adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin) → (𝑓𝑠) ⊆ 𝑢)
9491, 93sylbi 220 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓𝑠) ⊆ 𝑢)
9590, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ⊆ 𝑢)
9695ralrimiva 3174 . . . . . . . . . . . . . . . . . 18 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
97 iunss 4944 . . . . . . . . . . . . . . . . . 18 ( 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢 ↔ ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
9896, 97sylibr 237 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
9998ad2antrl 727 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
100 simplrr 777 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑢)
101100snssd 4715 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
10299, 101unssd 4137 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
10390elin2d 4150 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ Fin)
104103ralrimiva 3174 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ∈ Fin)
105 iunfi 8800 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ Fin) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
10681, 104, 105syl2an 598 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
107106ad4ant14 751 . . . . . . . . . . . . . . . . 17 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
108107ad2ant2lr 747 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
109 snfi 8581 . . . . . . . . . . . . . . . 16 {𝑤} ∈ Fin
110 unfi 8773 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
111108, 109, 110sylancl 589 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
112102, 111jca 515 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
113 elin 3924 . . . . . . . . . . . . . . 15 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
11419elpw2 5224 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
115114anbi1i 626 . . . . . . . . . . . . . . 15 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
116113, 115bitr2i 279 . . . . . . . . . . . . . 14 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
117112, 116sylib 221 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
118 ralnex 3224 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
119118imbi2i 339 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
120119albii 1821 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
121 alinexa 1844 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
122120, 121bitr2i 279 . . . . . . . . . . . . . . . . . . . . 21 (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)))
123 fveq2 6652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 = 𝑧 → (𝑓𝑠) = (𝑓𝑧))
124123unieqd 4827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧 (𝑓𝑠) = (𝑓𝑧))
125 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧𝑠 = 𝑧)
126124, 125uneq12d 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = 𝑧 → ( (𝑓𝑠) ∪ 𝑠) = ( (𝑓𝑧) ∪ 𝑧))
127126eqeq2d 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = 𝑧 → (𝑋 = ( (𝑓𝑠) ∪ 𝑠) ↔ 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
128127rspcv 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
129 eleq2 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
130129biimpd 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
131 elun 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (𝑣 (𝑓𝑧) ∨ 𝑣𝑧))
132 eluni 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 (𝑓𝑧) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
133132orbi1i 911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑣 (𝑓𝑧) ∨ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧))
134 df-or 845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
135 alinexa 1844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) ↔ ¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
136135imbi1i 353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
137134, 136bitr4i 281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
138131, 133, 1373bitri 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
139 eleq2 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑤 → (𝑣𝑦𝑣𝑤))
140 eleq1w 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (𝑦 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑠)))
141140notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑠)))
142141ralbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑤 → (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
143139, 142imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑤 → ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠))))
144143spvv 2003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
145123eleq2d 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 → (𝑤 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑧)))
146145notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑧)))
147146rspcv 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧𝑡 → (∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠) → ¬ 𝑤 ∈ (𝑓𝑧)))
148144, 147syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
149148alrimdv 1930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
150149imim1d 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧𝑡 → ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
151138, 150syl5bi 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
152151a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧))))
153130, 152syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑡 → (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
154128, 153syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
155154com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
156155imp31 421 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
157156com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑧𝑡𝑣𝑧)))
158157ralrimdv 3178 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑧𝑡 𝑣𝑧))
159 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑣 ∈ V
160159elint2 4858 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 𝑡 ↔ ∀𝑧𝑡 𝑣𝑧)
161158, 160syl6ibr 255 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣 𝑡))
162 eleq2 2902 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑡 → (𝑣𝑤𝑣 𝑡))
163162ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑣𝑤𝑣 𝑡))
164161, 163sylibrd 262 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
165122, 164syl5bi 245 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
166165orrd 860 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤))
167166ex 416 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋 → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤)))
168 orc 864 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
169168anim2i 619 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
170169eximi 1836 . . . . . . . . . . . . . . . . . . . 20 (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
171 equid 2019 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 = 𝑤
172 vex 3472 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
173 equequ1 2032 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → (𝑦 = 𝑤𝑤 = 𝑤))
174139, 173anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑤 → ((𝑣𝑦𝑦 = 𝑤) ↔ (𝑣𝑤𝑤 = 𝑤)))
175172, 174spcev 3582 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣𝑤𝑤 = 𝑤) → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
176171, 175mpan2 690 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑤 → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
177 olc 865 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑤 → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
178177anim2i 619 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣𝑦𝑦 = 𝑤) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
179178eximi 1836 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑦(𝑣𝑦𝑦 = 𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
180176, 179syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑤 → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
181170, 180jaoi 854 . . . . . . . . . . . . . . . . . . 19 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
182 eluni 4816 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
183 elun 4100 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}))
184 eliun 4898 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
185 velsn 4555 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
186184, 185orbi12i 912 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
187183, 186bitri 278 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
188187anbi2i 625 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
189188exbii 1849 . . . . . . . . . . . . . . . . . . . 20 (∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
190182, 189bitr2i 279 . . . . . . . . . . . . . . . . . . 19 (∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
191181, 190sylib 221 . . . . . . . . . . . . . . . . . 18 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
192167, 191syl6 35 . . . . . . . . . . . . . . . . 17 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
193192ad5ant25 761 . . . . . . . . . . . . . . . 16 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
194193ad2ant2l 745 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
195194ssrdv 3948 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
196 elun 4100 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}))
197 eliun 4898 . . . . . . . . . . . . . . . . . . 19 (𝑣 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑣 ∈ (𝑓𝑠))
198 velsn 4555 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
199197, 198orbi12i 912 . . . . . . . . . . . . . . . . . 18 ((𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
200196, 199bitri 278 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
201 nfra1 3208 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)
202 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 𝑠 𝑣𝑋
203 rsp 3195 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
204 eqimss2 3999 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋)
205 elssuni 4843 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (𝑓𝑠) → 𝑣 (𝑓𝑠))
206 ssun3 4125 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
207205, 206syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
208 sstr 3950 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) ∧ ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣𝑋)
209208expcom 417 . . . . . . . . . . . . . . . . . . . . . 22 (( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) → 𝑣𝑋))
210204, 207, 209syl2im 40 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
211203, 210syl6 35 . . . . . . . . . . . . . . . . . . . 20 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡 → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋)))
212201, 202, 211rexlimd 3303 . . . . . . . . . . . . . . . . . . 19 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
213212ad2antll 728 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
214 elpwi 4520 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
215214ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → 𝑢 ⊆ (fi‘𝑥))
216215ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
217216, 100sseldd 3943 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
218 elssuni 4843 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (fi‘𝑥) → 𝑤 (fi‘𝑥))
219217, 218syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 (fi‘𝑥))
22057, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘(fi‘𝑥)) = (fi‘𝑥)
22160, 220syl6req 2874 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝐽)
222221, 67eqtr4di 2875 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝑋)
2232223ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (fi‘𝑥) = 𝑋)
224223ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (fi‘𝑥) = 𝑋)
225219, 224sseqtrd 3982 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑋)
226 sseq1 3967 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑣𝑋𝑤𝑋))
227225, 226syl5ibrcom 250 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 = 𝑤𝑣𝑋))
228213, 227jaod 856 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ((∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤) → 𝑣𝑋))
229200, 228syl5bi 245 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑣𝑋))
230229ralrimiv 3173 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
231 unissb 4845 . . . . . . . . . . . . . . 15 ( ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
232230, 231sylibr 237 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋)
233195, 232eqssd 3959 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
234 unieq 4824 . . . . . . . . . . . . . 14 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
235234rspceeqv 3613 . . . . . . . . . . . . 13 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
236117, 233, 235syl2anc 587 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
237236ex 416 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
238237exlimdv 1934 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
23979, 89, 2383syld 60 . . . . . . . . 9 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
2404, 239syl5bi 245 . . . . . . . 8 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
241 dfrex2 3227 . . . . . . . 8 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
242240, 241syl6ib 254 . . . . . . 7 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
243242con4d 115 . . . . . 6 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))
244243exp32 424 . . . . 5 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (𝑤𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
245244com24 95 . . . 4 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
246245exp32 424 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))))
247246imp45 433 . 2 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)))
248247imp31 421 1 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084  wal 1536   = wceq 1538  wex 1781  wcel 2114  wral 3130  wrex 3131  Vcvv 3469  cdif 3905  cun 3906  cin 3907  wss 3908  𝒫 cpw 4511  {csn 4539   cuni 4813   cint 4851   ciun 4894  wf 6330  cfv 6334  Fincfn 8496  ficfi 8862  topGenctg 16702  TopBasesctb 21548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-fin 8500  df-fi 8863  df-topgen 16708  df-bases 21549
This theorem is referenced by:  alexsubALTlem4  22653
  Copyright terms: Public domain W3C validator