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

Theorem alexsubALTlem3 21663
 Description: Lemma for alexsubALT 21665. 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 2979 . . . . . . . . . . 11 (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
21ralbii 2963 . . . . . . . . . 10 (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
3 ralnex 2975 . . . . . . . . . 10 (∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
42, 3bitr2i 264 . . . . . . . . 9 (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛)
5 elin 3758 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6 elpwi 4117 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
76adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8 uncom 3719 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
97, 8syl6sseq 3614 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10 ssundif 4004 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
119, 10sylib 207 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12 diffi 8077 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
1312adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
1411, 13jca 553 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
155, 14sylbi 206 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1615adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1716ad2antll 761 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18 elin 3758 . . . . . . . . . . . . . . . . 17 ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19 vex 3176 . . . . . . . . . . . . . . . . . . 19 𝑢 ∈ V
2019elpw2 4755 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
2120anbi1i 727 . . . . . . . . . . . . . . . . 17 (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
2218, 21bitr2i 264 . . . . . . . . . . . . . . . 16 (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
2317, 22sylib 207 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24 simprrr 801 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = 𝑛)
25 eldif 3550 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
2625simplbi2 653 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27 elun 3715 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28 orcom 401 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
2927, 28bitr4i 266 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30 df-or 384 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
3129, 30bitr2i 264 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3226, 31sylib 207 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑛𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3332ssriv 3572 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34 uniss 4394 . . . . . . . . . . . . . . . . . . 19 (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3533, 34mp1i 13 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36 uniun 4392 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ {𝑠})
37 vex 3176 . . . . . . . . . . . . . . . . . . . . 21 𝑠 ∈ V
3837unisn 4387 . . . . . . . . . . . . . . . . . . . 20 {𝑠} = 𝑠
3938uneq2i 3726 . . . . . . . . . . . . . . . . . . 19 ( (𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4036, 39eqtri 2632 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4135, 40syl6sseq 3614 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
4224, 41eqsstrd 3602 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
43 difss 3699 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∖ {𝑠}) ⊆ 𝑛
4443unissi 4397 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∖ {𝑠}) ⊆ 𝑛
45 sseq2 3590 . . . . . . . . . . . . . . . . . . . 20 (𝑋 = 𝑛 → ( (𝑛 ∖ {𝑠}) ⊆ 𝑋 (𝑛 ∖ {𝑠}) ⊆ 𝑛))
4644, 45mpbiri 247 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑛 (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4746adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4847ad2antll 761 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
49 inss1 3795 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝒫 𝑥 ∩ Fin) ⊆ 𝒫 𝑥
5049sseli 3564 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
5150elpwid 4118 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
5251ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) → 𝑡𝑥)
5352ad2antlr 759 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑡𝑥)
54 simprl 790 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑡)
5553, 54sseldd 3569 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑥)
56 elssuni 4403 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑥𝑠 𝑥)
5755, 56syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠 𝑥)
58 fibas 20592 . . . . . . . . . . . . . . . . . . . . 21 (fi‘𝑥) ∈ TopBases
59 unitg 20582 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
6058, 59mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
61 unieq 4380 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
62613ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6362ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝐽 = (topGen‘(fi‘𝑥)))
64 vex 3176 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
65 fiuni 8217 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = (fi‘𝑥))
6760, 63, 663eqtr4rd 2655 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝐽)
68 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19 𝑋 = 𝐽
6967, 68syl6eqr 2662 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝑋)
7057, 69sseqtrd 3604 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑋)
7148, 70unssd 3751 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ( (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
7242, 71eqssd 3585 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
73 unieq 4380 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 ∖ {𝑠}) → 𝑚 = (𝑛 ∖ {𝑠}))
7473uneq1d 3728 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 ∖ {𝑠}) → ( 𝑚𝑠) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
7574eqeq2d 2620 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑛 ∖ {𝑠}) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)))
7675rspcev 3282 . . . . . . . . . . . . . . 15 (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7723, 72, 76syl2anc 691 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7877expr 641 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7978expd 451 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))))
8079rexlimdv 3012 . . . . . . . . . . 11 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
8180ralimdva 2945 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
82 inss2 3796 . . . . . . . . . . . . . . 15 (𝒫 𝑥 ∩ Fin) ⊆ Fin
8382sseli 3564 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
8483adantr 480 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → 𝑡 ∈ Fin)
85 unieq 4380 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑓𝑠) → 𝑚 = (𝑓𝑠))
8685uneq1d 3728 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑓𝑠) → ( 𝑚𝑠) = ( (𝑓𝑠) ∪ 𝑠))
8786eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑚 = (𝑓𝑠) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8887ac6sfi 8089 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8988ex 449 . . . . . . . . . . . . 13 (𝑡 ∈ Fin → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9084, 89syl 17 . . . . . . . . . . . 12 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9190adantr 480 . . . . . . . . . . 11 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
9291ad2antrl 760 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
93 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin))
94 elin 3758 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin))
95 elpwi 4117 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑠) ∈ 𝒫 𝑢 → (𝑓𝑠) ⊆ 𝑢)
9695adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin) → (𝑓𝑠) ⊆ 𝑢)
9794, 96sylbi 206 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓𝑠) ⊆ 𝑢)
9893, 97syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ⊆ 𝑢)
9998ralrimiva 2949 . . . . . . . . . . . . . . . . . 18 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
100 iunss 4497 . . . . . . . . . . . . . . . . . 18 ( 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢 ↔ ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
10199, 100sylibr 223 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
102101ad2antrl 760 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
103 simplrr 797 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑢)
104103snssd 4281 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
105102, 104unssd 3751 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
106 inss2 3796 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑢 ∩ Fin) ⊆ Fin
107106, 93sseldi 3566 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ Fin)
108107ralrimiva 2949 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ∈ Fin)
109 iunfi 8137 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ Fin) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
11084, 108, 109syl2an 493 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
111110adantlr 747 . . . . . . . . . . . . . . . . . 18 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
112111adantlr 747 . . . . . . . . . . . . . . . . 17 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
113112ad2ant2lr 780 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
114 snfi 7923 . . . . . . . . . . . . . . . 16 {𝑤} ∈ Fin
115 unfi 8112 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
116113, 114, 115sylancl 693 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
117105, 116jca 553 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
118 elin 3758 . . . . . . . . . . . . . . 15 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
11919elpw2 4755 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
120119anbi1i 727 . . . . . . . . . . . . . . 15 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
121118, 120bitr2i 264 . . . . . . . . . . . . . 14 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
122117, 121sylib 207 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
123 ralnex 2975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
124123imbi2i 325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
125124albii 1737 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
126 alinexa 1759 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
127125, 126bitr2i 264 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)))
128 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 = 𝑧 → (𝑓𝑠) = (𝑓𝑧))
129128unieqd 4382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 = 𝑧 (𝑓𝑠) = (𝑓𝑧))
130 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 = 𝑧𝑠 = 𝑧)
131129, 130uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 = 𝑧 → ( (𝑓𝑠) ∪ 𝑠) = ( (𝑓𝑧) ∪ 𝑧))
132131eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧 → (𝑋 = ( (𝑓𝑠) ∪ 𝑠) ↔ 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
133132rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
134 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
135134biimpd 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
136 elun 3715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (𝑣 (𝑓𝑧) ∨ 𝑣𝑧))
137 eluni 4375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 (𝑓𝑧) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
138137orbi1i 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑣 (𝑓𝑧) ∨ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧))
139 df-or 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
140 alinexa 1759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) ↔ ¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
141140imbi1i 338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
142139, 141bitr4i 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
143136, 138, 1423bitri 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
144 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (𝑣𝑦𝑣𝑤))
145 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 = 𝑤 → (𝑦 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑠)))
146145notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑠)))
147146ralbidv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
148144, 147imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑤 → ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠))))
149148spv 2248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
150128eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 = 𝑧 → (𝑤 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑧)))
151150notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑧)))
152151rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧𝑡 → (∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠) → ¬ 𝑤 ∈ (𝑓𝑧)))
153149, 152syl9r 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
154153alrimdv 1844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
155154imim1d 80 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑡 → ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
156143, 155syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
157156a1dd 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧))))
158135, 157syl9r 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
159133, 158syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
160159com14 94 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
161160imp31 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
162161com23 84 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑧𝑡𝑣𝑧)))
163162ralrimdv 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑧𝑡 𝑣𝑧))
164 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑣 ∈ V
165164elint2 4417 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑡 ↔ ∀𝑧𝑡 𝑣𝑧)
166163, 165syl6ibr 241 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣 𝑡))
167 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑡 → (𝑣𝑤𝑣 𝑡))
168167ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑣𝑤𝑣 𝑡))
169166, 168sylibrd 248 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
170127, 169syl5bi 231 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
171170orrd 392 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤))
172171ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋 → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤)))
173 orc 399 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
174173anim2i 591 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
175174eximi 1752 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
176 equid 1926 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 = 𝑤
177 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
178 equequ1 1939 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑤 → (𝑦 = 𝑤𝑤 = 𝑤))
179144, 178anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → ((𝑣𝑦𝑦 = 𝑤) ↔ (𝑣𝑤𝑤 = 𝑤)))
180177, 179spcev 3273 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣𝑤𝑤 = 𝑤) → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
181176, 180mpan2 703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣𝑤 → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
182 olc 398 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
183182anim2i 591 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣𝑦𝑦 = 𝑤) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
184183eximi 1752 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑦(𝑣𝑦𝑦 = 𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝑤 → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
186175, 185jaoi 393 . . . . . . . . . . . . . . . . . . . . 21 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
187 eluni 4375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
188 elun 3715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}))
189 eliun 4460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
190 velsn 4141 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
191189, 190orbi12i 542 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
192188, 191bitri 263 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
193192anbi2i 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
194193exbii 1764 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
195187, 194bitr2i 264 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
196186, 195sylib 207 . . . . . . . . . . . . . . . . . . . 20 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
197172, 196syl6 34 . . . . . . . . . . . . . . . . . . 19 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
198197adantll 746 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
199198adantlr 747 . . . . . . . . . . . . . . . . 17 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
200199adantlr 747 . . . . . . . . . . . . . . . 16 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
201200ad2ant2l 778 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
202201ssrdv 3574 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
203 elun 3715 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}))
204 eliun 4460 . . . . . . . . . . . . . . . . . . 19 (𝑣 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑣 ∈ (𝑓𝑠))
205 velsn 4141 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
206204, 205orbi12i 542 . . . . . . . . . . . . . . . . . 18 ((𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
207203, 206bitri 263 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
208 nfra1 2925 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)
209 nfv 1830 . . . . . . . . . . . . . . . . . . . 20 𝑠 𝑣𝑋
210 rsp 2913 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
211 eqimss2 3621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋)
212 elssuni 4403 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (𝑓𝑠) → 𝑣 (𝑓𝑠))
213 ssun3 3740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
214212, 213syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
215 sstr 3576 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) ∧ ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣𝑋)
216215expcom 450 . . . . . . . . . . . . . . . . . . . . . 22 (( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) → 𝑣𝑋))
217211, 214, 216syl2im 39 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
218210, 217syl6 34 . . . . . . . . . . . . . . . . . . . 20 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡 → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋)))
219208, 209, 218rexlimd 3008 . . . . . . . . . . . . . . . . . . 19 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
220219ad2antll 761 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
221 elpwi 4117 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
222221ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → 𝑢 ⊆ (fi‘𝑥))
223222ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
224223, 103sseldd 3569 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
225 elssuni 4403 . . . . . . . . . . . . . . . . . . . . 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 2661 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝐽)
229228, 68syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝑋)
2302293ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (fi‘𝑥) = 𝑋)
231230ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (fi‘𝑥) = 𝑋)
232226, 231sseqtrd 3604 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑋)
233 sseq1 3589 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑣𝑋𝑤𝑋))
234232, 233syl5ibrcom 236 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 = 𝑤𝑣𝑋))
235220, 234jaod 394 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ((∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤) → 𝑣𝑋))
236207, 235syl5bi 231 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑣𝑋))
237236ralrimiv 2948 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
238 unissb 4405 . . . . . . . . . . . . . . 15 ( ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
239237, 238sylibr 223 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋)
240202, 239eqssd 3585 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
241 unieq 4380 . . . . . . . . . . . . . . 15 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
242241eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → (𝑋 = 𝑏𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
243242rspcev 3282 . . . . . . . . . . . . 13 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
244122, 240, 243syl2anc 691 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
245244ex 449 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
246245exlimdv 1848 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
24781, 92, 2463syld 58 . . . . . . . . 9 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
2484, 247syl5bi 231 . . . . . . . 8 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
249 dfrex2 2979 . . . . . . . 8 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
250248, 249syl6ib 240 . . . . . . 7 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
251250con4d 113 . . . . . 6 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))
252251exp32 629 . . . . 5 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (𝑤𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
253252com24 93 . . . 4 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
254253exp32 629 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))))
255254imp45 621 . 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 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∩ cint 4410  ∪ ciun 4455  ⟶wf 5800  ‘cfv 5804  Fincfn 7841  ficfi 8199  topGenctg 15921  TopBasesctb 20520 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-topgen 15927  df-bases 20522 This theorem is referenced by:  alexsubALTlem4  21664
 Copyright terms: Public domain W3C validator