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

Theorem alexsubALTlem3 22075
Description: Lemma for alexsubALT 22077. 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 3135 . . . . . . . . . . 11 (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
21ralbii 3119 . . . . . . . . . 10 (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
3 ralnex 3131 . . . . . . . . . 10 (∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
42, 3bitr2i 265 . . . . . . . . 9 (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛)
5 elin 3940 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6 elpwi 4313 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
76adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8 uncom 3901 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
97, 8syl6sseq 3793 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10 ssundif 4197 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
119, 10sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12 diffi 8360 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
1312adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
1411, 13jca 555 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
155, 14sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1615adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1716ad2antll 767 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18 elin 3940 . . . . . . . . . . . . . . . . 17 ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19 vex 3344 . . . . . . . . . . . . . . . . . . 19 𝑢 ∈ V
2019elpw2 4978 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
2120anbi1i 733 . . . . . . . . . . . . . . . . 17 (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
2218, 21bitr2i 265 . . . . . . . . . . . . . . . 16 (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
2317, 22sylib 208 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24 simprrr 824 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = 𝑛)
25 eldif 3726 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
2625simplbi2 656 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27 elun 3897 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28 orcom 401 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
2927, 28bitr4i 267 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30 df-or 384 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
3129, 30bitr2i 265 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3226, 31sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑛𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3332ssriv 3749 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34 uniss 4611 . . . . . . . . . . . . . . . . . . 19 (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3533, 34mp1i 13 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36 uniun 4609 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ {𝑠})
37 vex 3344 . . . . . . . . . . . . . . . . . . . . 21 𝑠 ∈ V
3837unisn 4604 . . . . . . . . . . . . . . . . . . . 20 {𝑠} = 𝑠
3938uneq2i 3908 . . . . . . . . . . . . . . . . . . 19 ( (𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4036, 39eqtri 2783 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4135, 40syl6sseq 3793 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
4224, 41eqsstrd 3781 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
43 difss 3881 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∖ {𝑠}) ⊆ 𝑛
4443unissi 4614 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∖ {𝑠}) ⊆ 𝑛
45 sseq2 3769 . . . . . . . . . . . . . . . . . . . 20 (𝑋 = 𝑛 → ( (𝑛 ∖ {𝑠}) ⊆ 𝑋 (𝑛 ∖ {𝑠}) ⊆ 𝑛))
4644, 45mpbiri 248 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑛 (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4746adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4847ad2antll 767 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
49 inss1 3977 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝒫 𝑥 ∩ Fin) ⊆ 𝒫 𝑥
5049sseli 3741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
5150elpwid 4315 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
5251ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) → 𝑡𝑥)
5352ad2antlr 765 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑡𝑥)
54 simprl 811 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑡)
5553, 54sseldd 3746 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑥)
56 elssuni 4620 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑥𝑠 𝑥)
5755, 56syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠 𝑥)
58 fibas 21004 . . . . . . . . . . . . . . . . . . . . 21 (fi‘𝑥) ∈ TopBases
59 unitg 20994 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
6058, 59mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
61 unieq 4597 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
62613ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6362ad3antrrr 768 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝐽 = (topGen‘(fi‘𝑥)))
64 vex 3344 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
65 fiuni 8502 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = (fi‘𝑥))
6760, 63, 663eqtr4rd 2806 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝐽)
68 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19 𝑋 = 𝐽
6967, 68syl6eqr 2813 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝑋)
7057, 69sseqtrd 3783 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑋)
7148, 70unssd 3933 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ( (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
7242, 71eqssd 3762 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
73 unieq 4597 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 ∖ {𝑠}) → 𝑚 = (𝑛 ∖ {𝑠}))
7473uneq1d 3910 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 ∖ {𝑠}) → ( 𝑚𝑠) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
7574eqeq2d 2771 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑛 ∖ {𝑠}) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)))
7675rspcev 3450 . . . . . . . . . . . . . . 15 (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7723, 72, 76syl2anc 696 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7877expr 644 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7978expd 451 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))))
8079rexlimdv 3169 . . . . . . . . . . 11 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
8180ralimdva 3101 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
82 inss2 3978 . . . . . . . . . . . . . . 15 (𝒫 𝑥 ∩ Fin) ⊆ Fin
8382sseli 3741 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
8483adantr 472 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → 𝑡 ∈ Fin)
85 unieq 4597 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑓𝑠) → 𝑚 = (𝑓𝑠))
8685uneq1d 3910 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑓𝑠) → ( 𝑚𝑠) = ( (𝑓𝑠) ∪ 𝑠))
8786eqeq2d 2771 . . . . . . . . . . . . . . 15 (𝑚 = (𝑓𝑠) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8887ac6sfi 8372 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8988ex 449 . . . . . . . . . . . . 13 (𝑡 ∈ Fin → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9084, 89syl 17 . . . . . . . . . . . 12 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9190adantr 472 . . . . . . . . . . 11 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9291ad2antrl 766 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
93 ffvelrn 6522 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin))
94 elin 3940 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin))
95 elpwi 4313 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑠) ∈ 𝒫 𝑢 → (𝑓𝑠) ⊆ 𝑢)
9695adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin) → (𝑓𝑠) ⊆ 𝑢)
9794, 96sylbi 207 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓𝑠) ⊆ 𝑢)
9893, 97syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ⊆ 𝑢)
9998ralrimiva 3105 . . . . . . . . . . . . . . . . . 18 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
100 iunss 4714 . . . . . . . . . . . . . . . . . 18 ( 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢 ↔ ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
10199, 100sylibr 224 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
102101ad2antrl 766 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
103 simplrr 820 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑢)
104103snssd 4486 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
105102, 104unssd 3933 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
106 inss2 3978 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑢 ∩ Fin) ⊆ Fin
107106, 93sseldi 3743 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ Fin)
108107ralrimiva 3105 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ∈ Fin)
109 iunfi 8422 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ Fin) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
11084, 108, 109syl2an 495 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
111110adantlr 753 . . . . . . . . . . . . . . . . . 18 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
112111adantlr 753 . . . . . . . . . . . . . . . . 17 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
113112ad2ant2lr 801 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
114 snfi 8206 . . . . . . . . . . . . . . . 16 {𝑤} ∈ Fin
115 unfi 8395 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
116113, 114, 115sylancl 697 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
117105, 116jca 555 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
118 elin 3940 . . . . . . . . . . . . . . 15 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
11919elpw2 4978 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
120119anbi1i 733 . . . . . . . . . . . . . . 15 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
121118, 120bitr2i 265 . . . . . . . . . . . . . 14 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
122117, 121sylib 208 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
123 ralnex 3131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
124123imbi2i 325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
125124albii 1896 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
126 alinexa 1919 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
127125, 126bitr2i 265 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)))
128 fveq2 6354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 = 𝑧 → (𝑓𝑠) = (𝑓𝑧))
129128unieqd 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 = 𝑧 (𝑓𝑠) = (𝑓𝑧))
130 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 = 𝑧𝑠 = 𝑧)
131129, 130uneq12d 3912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 = 𝑧 → ( (𝑓𝑠) ∪ 𝑠) = ( (𝑓𝑧) ∪ 𝑧))
132131eqeq2d 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧 → (𝑋 = ( (𝑓𝑠) ∪ 𝑠) ↔ 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
133132rspcv 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
134 eleq2 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
135134biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
136 elun 3897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (𝑣 (𝑓𝑧) ∨ 𝑣𝑧))
137 eluni 4592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 (𝑓𝑧) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
138137orbi1i 543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑣 (𝑓𝑧) ∨ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧))
139 df-or 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
140 alinexa 1919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) ↔ ¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
141140imbi1i 338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
142139, 141bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
143136, 138, 1423bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
144 eleq2 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (𝑣𝑦𝑣𝑤))
145 eleq1w 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 = 𝑤 → (𝑦 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑠)))
146145notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑠)))
147146ralbidv 3125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
148144, 147imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑤 → ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠))))
149148spv 2406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
150128eleq2d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 = 𝑧 → (𝑤 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑧)))
151150notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑧)))
152151rspcv 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧𝑡 → (∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠) → ¬ 𝑤 ∈ (𝑓𝑧)))
153149, 152syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
154153alrimdv 2007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
155154imim1d 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑡 → ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
156143, 155syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
157156a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧))))
158135, 157syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
159133, 158syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
160159com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
161160imp31 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
162161com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑧𝑡𝑣𝑧)))
163162ralrimdv 3107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑧𝑡 𝑣𝑧))
164 vex 3344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑣 ∈ V
165164elint2 4635 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑡 ↔ ∀𝑧𝑡 𝑣𝑧)
166163, 165syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣 𝑡))
167 eleq2 2829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑡 → (𝑣𝑤𝑣 𝑡))
168167ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑣𝑤𝑣 𝑡))
169166, 168sylibrd 249 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
170127, 169syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
171170orrd 392 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤))
172171ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋 → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤)))
173 orc 399 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
174173anim2i 594 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
175174eximi 1911 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
176 equid 2095 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 = 𝑤
177 vex 3344 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
178 equequ1 2108 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑤 → (𝑦 = 𝑤𝑤 = 𝑤))
179144, 178anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → ((𝑣𝑦𝑦 = 𝑤) ↔ (𝑣𝑤𝑤 = 𝑤)))
180177, 179spcev 3441 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣𝑤𝑤 = 𝑤) → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
181176, 180mpan2 709 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣𝑤 → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
182 olc 398 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
183182anim2i 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣𝑦𝑦 = 𝑤) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
184183eximi 1911 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑦(𝑣𝑦𝑦 = 𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝑤 → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
186175, 185jaoi 393 . . . . . . . . . . . . . . . . . . . . 21 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
187 eluni 4592 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
188 elun 3897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}))
189 eliun 4677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
190 velsn 4338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
191189, 190orbi12i 544 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
192188, 191bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
193192anbi2i 732 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
194193exbii 1923 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
195187, 194bitr2i 265 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
196186, 195sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
197172, 196syl6 35 . . . . . . . . . . . . . . . . . . 19 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
198197adantll 752 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
199198adantlr 753 . . . . . . . . . . . . . . . . 17 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
200199adantlr 753 . . . . . . . . . . . . . . . 16 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
201200ad2ant2l 799 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
202201ssrdv 3751 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
203 elun 3897 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}))
204 eliun 4677 . . . . . . . . . . . . . . . . . . 19 (𝑣 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑣 ∈ (𝑓𝑠))
205 velsn 4338 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
206204, 205orbi12i 544 . . . . . . . . . . . . . . . . . 18 ((𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
207203, 206bitri 264 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
208 nfra1 3080 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)
209 nfv 1993 . . . . . . . . . . . . . . . . . . . 20 𝑠 𝑣𝑋
210 rsp 3068 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
211 eqimss2 3800 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋)
212 elssuni 4620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (𝑓𝑠) → 𝑣 (𝑓𝑠))
213 ssun3 3922 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
214212, 213syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
215 sstr 3753 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) ∧ ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣𝑋)
216215expcom 450 . . . . . . . . . . . . . . . . . . . . . 22 (( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) → 𝑣𝑋))
217211, 214, 216syl2im 40 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
218210, 217syl6 35 . . . . . . . . . . . . . . . . . . . 20 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡 → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋)))
219208, 209, 218rexlimd 3165 . . . . . . . . . . . . . . . . . . 19 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
220219ad2antll 767 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
221 elpwi 4313 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
222221ad2antrl 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → 𝑢 ⊆ (fi‘𝑥))
223222ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
224223, 103sseldd 3746 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
225 elssuni 4620 . . . . . . . . . . . . . . . . . . . . 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 2812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝐽)
229228, 68syl6eqr 2813 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝑋)
2302293ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (fi‘𝑥) = 𝑋)
231230ad3antrrr 768 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (fi‘𝑥) = 𝑋)
232226, 231sseqtrd 3783 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑋)
233 sseq1 3768 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑣𝑋𝑤𝑋))
234232, 233syl5ibrcom 237 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 = 𝑤𝑣𝑋))
235220, 234jaod 394 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ((∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤) → 𝑣𝑋))
236207, 235syl5bi 232 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑣𝑋))
237236ralrimiv 3104 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
238 unissb 4622 . . . . . . . . . . . . . . 15 ( ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
239237, 238sylibr 224 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋)
240202, 239eqssd 3762 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
241 unieq 4597 . . . . . . . . . . . . . . 15 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
242241eqeq2d 2771 . . . . . . . . . . . . . 14 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → (𝑋 = 𝑏𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
243242rspcev 3450 . . . . . . . . . . . . 13 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
244122, 240, 243syl2anc 696 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
245244ex 449 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
246245exlimdv 2011 . . . . . . . . . 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 3135 . . . . . . . 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 632 . . . . 5 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (𝑤𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
253252com24 95 . . . 4 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
254253exp32 632 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))))
255254imp45 624 . 2 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)))
256255imp31 447 1 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072  wal 1630   = wceq 1632  wex 1853  wcel 2140  wral 3051  wrex 3052  Vcvv 3341  cdif 3713  cun 3714  cin 3715  wss 3716  𝒫 cpw 4303  {csn 4322   cuni 4589   cint 4628   ciun 4673  wf 6046  cfv 6050  Fincfn 8124  ficfi 8484  topGenctg 16321  TopBasesctb 20972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-om 7233  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-1o 7731  df-oadd 7735  df-er 7914  df-en 8125  df-fin 8128  df-fi 8485  df-topgen 16327  df-bases 20973
This theorem is referenced by:  alexsubALTlem4  22076
  Copyright terms: Public domain W3C validator