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

Theorem alexsubALTlem3 21763
Description: Lemma for alexsubALT 21765. 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 2990 . . . . . . . . . . 11 (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
21ralbii 2974 . . . . . . . . . 10 (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
3 ralnex 2986 . . . . . . . . . 10 (∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
42, 3bitr2i 265 . . . . . . . . 9 (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛)
5 elin 3774 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6 elpwi 4140 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
76adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8 uncom 3735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
97, 8syl6sseq 3630 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10 ssundif 4024 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
119, 10sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12 diffi 8136 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
1312adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
1411, 13jca 554 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
155, 14sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1615adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1716ad2antll 764 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18 elin 3774 . . . . . . . . . . . . . . . . 17 ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19 vex 3189 . . . . . . . . . . . . . . . . . . 19 𝑢 ∈ V
2019elpw2 4788 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
2120anbi1i 730 . . . . . . . . . . . . . . . . 17 (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
2218, 21bitr2i 265 . . . . . . . . . . . . . . . 16 (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
2317, 22sylib 208 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24 simprrr 804 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = 𝑛)
25 eldif 3565 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
2625simplbi2 654 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27 elun 3731 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28 orcom 402 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
2927, 28bitr4i 267 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30 df-or 385 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
3129, 30bitr2i 265 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3226, 31sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑛𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3332ssriv 3587 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34 uniss 4424 . . . . . . . . . . . . . . . . . . 19 (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3533, 34mp1i 13 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36 uniun 4422 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ {𝑠})
37 vex 3189 . . . . . . . . . . . . . . . . . . . . 21 𝑠 ∈ V
3837unisn 4417 . . . . . . . . . . . . . . . . . . . 20 {𝑠} = 𝑠
3938uneq2i 3742 . . . . . . . . . . . . . . . . . . 19 ( (𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4036, 39eqtri 2643 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4135, 40syl6sseq 3630 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
4224, 41eqsstrd 3618 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
43 difss 3715 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∖ {𝑠}) ⊆ 𝑛
4443unissi 4427 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∖ {𝑠}) ⊆ 𝑛
45 sseq2 3606 . . . . . . . . . . . . . . . . . . . 20 (𝑋 = 𝑛 → ( (𝑛 ∖ {𝑠}) ⊆ 𝑋 (𝑛 ∖ {𝑠}) ⊆ 𝑛))
4644, 45mpbiri 248 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑛 (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4746adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4847ad2antll 764 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
49 inss1 3811 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝒫 𝑥 ∩ Fin) ⊆ 𝒫 𝑥
5049sseli 3579 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
5150elpwid 4141 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
5251ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) → 𝑡𝑥)
5352ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑡𝑥)
54 simprl 793 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑡)
5553, 54sseldd 3584 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑥)
56 elssuni 4433 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑥𝑠 𝑥)
5755, 56syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠 𝑥)
58 fibas 20692 . . . . . . . . . . . . . . . . . . . . 21 (fi‘𝑥) ∈ TopBases
59 unitg 20682 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
6058, 59mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
61 unieq 4410 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
62613ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6362ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝐽 = (topGen‘(fi‘𝑥)))
64 vex 3189 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
65 fiuni 8278 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = (fi‘𝑥))
6760, 63, 663eqtr4rd 2666 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝐽)
68 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19 𝑋 = 𝐽
6967, 68syl6eqr 2673 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝑋)
7057, 69sseqtrd 3620 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑋)
7148, 70unssd 3767 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ( (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
7242, 71eqssd 3600 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
73 unieq 4410 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 ∖ {𝑠}) → 𝑚 = (𝑛 ∖ {𝑠}))
7473uneq1d 3744 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 ∖ {𝑠}) → ( 𝑚𝑠) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
7574eqeq2d 2631 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑛 ∖ {𝑠}) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)))
7675rspcev 3295 . . . . . . . . . . . . . . 15 (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7723, 72, 76syl2anc 692 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7877expr 642 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7978expd 452 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))))
8079rexlimdv 3023 . . . . . . . . . . 11 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
8180ralimdva 2956 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
82 inss2 3812 . . . . . . . . . . . . . . 15 (𝒫 𝑥 ∩ Fin) ⊆ Fin
8382sseli 3579 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
8483adantr 481 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → 𝑡 ∈ Fin)
85 unieq 4410 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑓𝑠) → 𝑚 = (𝑓𝑠))
8685uneq1d 3744 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑓𝑠) → ( 𝑚𝑠) = ( (𝑓𝑠) ∪ 𝑠))
8786eqeq2d 2631 . . . . . . . . . . . . . . 15 (𝑚 = (𝑓𝑠) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8887ac6sfi 8148 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8988ex 450 . . . . . . . . . . . . 13 (𝑡 ∈ Fin → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9084, 89syl 17 . . . . . . . . . . . 12 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9190adantr 481 . . . . . . . . . . 11 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9291ad2antrl 763 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
93 ffvelrn 6313 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin))
94 elin 3774 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin))
95 elpwi 4140 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑠) ∈ 𝒫 𝑢 → (𝑓𝑠) ⊆ 𝑢)
9695adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin) → (𝑓𝑠) ⊆ 𝑢)
9794, 96sylbi 207 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓𝑠) ⊆ 𝑢)
9893, 97syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ⊆ 𝑢)
9998ralrimiva 2960 . . . . . . . . . . . . . . . . . 18 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
100 iunss 4527 . . . . . . . . . . . . . . . . . 18 ( 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢 ↔ ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
10199, 100sylibr 224 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
102101ad2antrl 763 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
103 simplrr 800 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑢)
104103snssd 4309 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
105102, 104unssd 3767 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
106 inss2 3812 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑢 ∩ Fin) ⊆ Fin
107106, 93sseldi 3581 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ Fin)
108107ralrimiva 2960 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ∈ Fin)
109 iunfi 8198 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ Fin) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
11084, 108, 109syl2an 494 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
111110adantlr 750 . . . . . . . . . . . . . . . . . 18 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
112111adantlr 750 . . . . . . . . . . . . . . . . 17 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
113112ad2ant2lr 783 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
114 snfi 7982 . . . . . . . . . . . . . . . 16 {𝑤} ∈ Fin
115 unfi 8171 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
116113, 114, 115sylancl 693 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
117105, 116jca 554 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
118 elin 3774 . . . . . . . . . . . . . . 15 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
11919elpw2 4788 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
120119anbi1i 730 . . . . . . . . . . . . . . 15 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
121118, 120bitr2i 265 . . . . . . . . . . . . . 14 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
122117, 121sylib 208 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
123 ralnex 2986 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
124123imbi2i 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
125124albii 1744 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
126 alinexa 1767 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
127125, 126bitr2i 265 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)))
128 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 = 𝑧 → (𝑓𝑠) = (𝑓𝑧))
129128unieqd 4412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 = 𝑧 (𝑓𝑠) = (𝑓𝑧))
130 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 = 𝑧𝑠 = 𝑧)
131129, 130uneq12d 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 = 𝑧 → ( (𝑓𝑠) ∪ 𝑠) = ( (𝑓𝑧) ∪ 𝑧))
132131eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧 → (𝑋 = ( (𝑓𝑠) ∪ 𝑠) ↔ 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
133132rspcv 3291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
134 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
135134biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
136 elun 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (𝑣 (𝑓𝑧) ∨ 𝑣𝑧))
137 eluni 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 (𝑓𝑧) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
138137orbi1i 542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑣 (𝑓𝑧) ∨ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧))
139 df-or 385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
140 alinexa 1767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) ↔ ¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
141140imbi1i 339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
142139, 141bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
143136, 138, 1423bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
144 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (𝑣𝑦𝑣𝑤))
145 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 = 𝑤 → (𝑦 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑠)))
146145notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑠)))
147146ralbidv 2980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
148144, 147imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑤 → ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠))))
149148spv 2259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
150128eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 = 𝑧 → (𝑤 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑧)))
151150notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑧)))
152151rspcv 3291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧𝑡 → (∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠) → ¬ 𝑤 ∈ (𝑓𝑧)))
153149, 152syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
154153alrimdv 1854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
155154imim1d 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑡 → ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
156143, 155syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
157156a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧))))
158135, 157syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
159133, 158syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
160159com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
161160imp31 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
162161com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑧𝑡𝑣𝑧)))
163162ralrimdv 2962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑧𝑡 𝑣𝑧))
164 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑣 ∈ V
165164elint2 4447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑡 ↔ ∀𝑧𝑡 𝑣𝑧)
166163, 165syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣 𝑡))
167 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑡 → (𝑣𝑤𝑣 𝑡))
168167ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑣𝑤𝑣 𝑡))
169166, 168sylibrd 249 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
170127, 169syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
171170orrd 393 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤))
172171ex 450 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋 → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤)))
173 orc 400 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
174173anim2i 592 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
175174eximi 1759 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
176 equid 1936 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 = 𝑤
177 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
178 equequ1 1949 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑤 → (𝑦 = 𝑤𝑤 = 𝑤))
179144, 178anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → ((𝑣𝑦𝑦 = 𝑤) ↔ (𝑣𝑤𝑤 = 𝑤)))
180177, 179spcev 3286 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣𝑤𝑤 = 𝑤) → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
181176, 180mpan2 706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣𝑤 → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
182 olc 399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
183182anim2i 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣𝑦𝑦 = 𝑤) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
184183eximi 1759 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑦(𝑣𝑦𝑦 = 𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝑤 → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
186175, 185jaoi 394 . . . . . . . . . . . . . . . . . . . . 21 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
187 eluni 4405 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
188 elun 3731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}))
189 eliun 4490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
190 velsn 4164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
191189, 190orbi12i 543 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
192188, 191bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
193192anbi2i 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
194193exbii 1771 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
195187, 194bitr2i 265 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
196186, 195sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
197172, 196syl6 35 . . . . . . . . . . . . . . . . . . 19 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
198197adantll 749 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
199198adantlr 750 . . . . . . . . . . . . . . . . 17 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
200199adantlr 750 . . . . . . . . . . . . . . . 16 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
201200ad2ant2l 781 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
202201ssrdv 3589 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
203 elun 3731 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}))
204 eliun 4490 . . . . . . . . . . . . . . . . . . 19 (𝑣 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑣 ∈ (𝑓𝑠))
205 velsn 4164 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
206204, 205orbi12i 543 . . . . . . . . . . . . . . . . . 18 ((𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
207203, 206bitri 264 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
208 nfra1 2936 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)
209 nfv 1840 . . . . . . . . . . . . . . . . . . . 20 𝑠 𝑣𝑋
210 rsp 2924 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
211 eqimss2 3637 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋)
212 elssuni 4433 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (𝑓𝑠) → 𝑣 (𝑓𝑠))
213 ssun3 3756 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
214212, 213syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
215 sstr 3591 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) ∧ ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣𝑋)
216215expcom 451 . . . . . . . . . . . . . . . . . . . . . 22 (( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) → 𝑣𝑋))
217211, 214, 216syl2im 40 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
218210, 217syl6 35 . . . . . . . . . . . . . . . . . . . 20 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡 → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋)))
219208, 209, 218rexlimd 3019 . . . . . . . . . . . . . . . . . . 19 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
220219ad2antll 764 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
221 elpwi 4140 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
222221ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → 𝑢 ⊆ (fi‘𝑥))
223222ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
224223, 103sseldd 3584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
225 elssuni 4433 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (fi‘𝑥) → 𝑤 (fi‘𝑥))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 (fi‘𝑥))
22758, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘(fi‘𝑥)) = (fi‘𝑥)
22861, 227syl6req 2672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝐽)
229228, 68syl6eqr 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝑋)
2302293ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (fi‘𝑥) = 𝑋)
231230ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (fi‘𝑥) = 𝑋)
232226, 231sseqtrd 3620 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑋)
233 sseq1 3605 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑣𝑋𝑤𝑋))
234232, 233syl5ibrcom 237 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 = 𝑤𝑣𝑋))
235220, 234jaod 395 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ((∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤) → 𝑣𝑋))
236207, 235syl5bi 232 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑣𝑋))
237236ralrimiv 2959 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
238 unissb 4435 . . . . . . . . . . . . . . 15 ( ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
239237, 238sylibr 224 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋)
240202, 239eqssd 3600 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
241 unieq 4410 . . . . . . . . . . . . . . 15 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
242241eqeq2d 2631 . . . . . . . . . . . . . 14 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → (𝑋 = 𝑏𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
243242rspcev 3295 . . . . . . . . . . . . 13 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
244122, 240, 243syl2anc 692 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
245244ex 450 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
246245exlimdv 1858 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
24781, 92, 2463syld 60 . . . . . . . . 9 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
2484, 247syl5bi 232 . . . . . . . 8 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
249 dfrex2 2990 . . . . . . . 8 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
250248, 249syl6ib 241 . . . . . . 7 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
251250con4d 114 . . . . . 6 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))
252251exp32 630 . . . . 5 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (𝑤𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
253252com24 95 . . . 4 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
254253exp32 630 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))))
255254imp45 622 . 2 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)))
256255imp31 448 1 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  𝒫 cpw 4130  {csn 4148   cuni 4402   cint 4440   ciun 4485  wf 5843  cfv 5847  Fincfn 7899  ficfi 8260  topGenctg 16019  TopBasesctb 20620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-fin 7903  df-fi 8261  df-topgen 16025  df-bases 20622
This theorem is referenced by:  alexsubALTlem4  21764
  Copyright terms: Public domain W3C validator