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

Theorem alexsubALTlem3 23400
Description: Lemma for alexsubALT 23402. 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 3076 . . . . . . . . . . 11 (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
21ralbii 3096 . . . . . . . . . 10 (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 ↔ ∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
3 ralnex 3075 . . . . . . . . . 10 (∀𝑠𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
42, 3bitr2i 275 . . . . . . . . 9 (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 ↔ ∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛)
5 elin 3926 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6 elpwi 4567 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
76adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8 uncom 4113 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
97, 8sseqtrdi 3994 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10 ssundif 4445 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
119, 10sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12 diffi 9123 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
1312adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
1411, 13jca 512 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
155, 14sylbi 216 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1615adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
1716ad2antll 727 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18 elin 3926 . . . . . . . . . . . . . . . . 17 ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑢 ∈ V
2019elpw2 5302 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
2120anbi1i 624 . . . . . . . . . . . . . . . . 17 (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
2218, 21bitr2i 275 . . . . . . . . . . . . . . . 16 (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
2317, 22sylib 217 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24 simprrr 780 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = 𝑛)
25 eldif 3920 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
2625simplbi2 501 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27 elun 4108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28 orcom 868 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
2927, 28bitr4i 277 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30 df-or 846 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
3129, 30bitr2i 275 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3226, 31sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑛𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3332ssriv 3948 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34 uniss 4873 . . . . . . . . . . . . . . . . . . 19 (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
3533, 34mp1i 13 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36 uniun 4891 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ {𝑠})
37 unisnv 4888 . . . . . . . . . . . . . . . . . . . 20 {𝑠} = 𝑠
3837uneq2i 4120 . . . . . . . . . . . . . . . . . . 19 ( (𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
3936, 38eqtri 2764 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)
4035, 39sseqtrdi 3994 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑛 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
4124, 40eqsstrd 3982 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 ⊆ ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
42 difss 4091 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∖ {𝑠}) ⊆ 𝑛
4342unissi 4874 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∖ {𝑠}) ⊆ 𝑛
44 sseq2 3970 . . . . . . . . . . . . . . . . . . . 20 (𝑋 = 𝑛 → ( (𝑛 ∖ {𝑠}) ⊆ 𝑋 (𝑛 ∖ {𝑠}) ⊆ 𝑛))
4543, 44mpbiri 257 . . . . . . . . . . . . . . . . . . 19 (𝑋 = 𝑛 (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4645adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
4746ad2antll 727 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (𝑛 ∖ {𝑠}) ⊆ 𝑋)
48 elinel1 4155 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
4948elpwid 4569 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡𝑥)
5049ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) → 𝑡𝑥)
5150ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑡𝑥)
52 simprl 769 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑡)
5351, 52sseldd 3945 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑥)
54 elssuni 4898 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑥𝑠 𝑥)
5553, 54syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠 𝑥)
56 fibas 22327 . . . . . . . . . . . . . . . . . . . . 21 (fi‘𝑥) ∈ TopBases
57 unitg 22317 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
5856, 57mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → (topGen‘(fi‘𝑥)) = (fi‘𝑥))
59 unieq 4876 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
60593ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → 𝐽 = (topGen‘(fi‘𝑥)))
6160ad3antrrr 728 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝐽 = (topGen‘(fi‘𝑥)))
62 vex 3449 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
63 fiuni 9364 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ V → 𝑥 = (fi‘𝑥))
6462, 63mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = (fi‘𝑥))
6558, 61, 643eqtr4rd 2787 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝐽)
66 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19 𝑋 = 𝐽
6765, 66eqtr4di 2794 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑥 = 𝑋)
6855, 67sseqtrd 3984 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑠𝑋)
6947, 68unssd 4146 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ( (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
7041, 69eqssd 3961 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
71 unieq 4876 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 ∖ {𝑠}) → 𝑚 = (𝑛 ∖ {𝑠}))
7271uneq1d 4122 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑛 ∖ {𝑠}) → ( 𝑚𝑠) = ( (𝑛 ∖ {𝑠}) ∪ 𝑠))
7372rspceeqv 3595 . . . . . . . . . . . . . . 15 (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7423, 70, 73syl2anc 584 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑠𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))
7574expr 457 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7675expd 416 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠))))
7776rexlimdv 3150 . . . . . . . . . . 11 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ 𝑠𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
7877ralimdva 3164 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)))
79 elinel2 4156 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
8079adantr 481 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → 𝑡 ∈ Fin)
81 unieq 4876 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑓𝑠) → 𝑚 = (𝑓𝑠))
8281uneq1d 4122 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑓𝑠) → ( 𝑚𝑠) = ( (𝑓𝑠) ∪ 𝑠))
8382eqeq2d 2747 . . . . . . . . . . . . . . 15 (𝑚 = (𝑓𝑠) → (𝑋 = ( 𝑚𝑠) ↔ 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8483ac6sfi 9231 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
8584ex 413 . . . . . . . . . . . . 13 (𝑡 ∈ Fin → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
8680, 85syl 17 . . . . . . . . . . . 12 ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
8786adantr 481 . . . . . . . . . . 11 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
8887ad2antrl 726 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ( 𝑚𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))))
89 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin))
90 elin 3926 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin))
91 elpwi 4567 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑠) ∈ 𝒫 𝑢 → (𝑓𝑠) ⊆ 𝑢)
9291adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓𝑠) ∈ 𝒫 𝑢 ∧ (𝑓𝑠) ∈ Fin) → (𝑓𝑠) ⊆ 𝑢)
9390, 92sylbi 216 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓𝑠) ⊆ 𝑢)
9489, 93syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ⊆ 𝑢)
9594ralrimiva 3143 . . . . . . . . . . . . . . . . . 18 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
96 iunss 5005 . . . . . . . . . . . . . . . . . 18 ( 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢 ↔ ∀𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
9795, 96sylibr 233 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
9897ad2antrl 726 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ⊆ 𝑢)
99 simplrr 776 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑢)
10099snssd 4769 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
10198, 100unssd 4146 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
10289elin2d 4159 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠𝑡) → (𝑓𝑠) ∈ Fin)
103102ralrimiva 3143 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠𝑡 (𝑓𝑠) ∈ Fin)
104 iunfi 9284 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ Fin) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
10580, 103, 104syl2an 596 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
106105ad4ant14 750 . . . . . . . . . . . . . . . . 17 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
107106ad2ant2lr 746 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑠𝑡 (𝑓𝑠) ∈ Fin)
108 snfi 8988 . . . . . . . . . . . . . . . 16 {𝑤} ∈ Fin
109 unfi 9116 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
110107, 108, 109sylancl 586 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin)
111101, 110jca 512 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
112 elin 3926 . . . . . . . . . . . . . . 15 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
11319elpw2 5302 . . . . . . . . . . . . . . . 16 (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢)
114113anbi1i 624 . . . . . . . . . . . . . . 15 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ (( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin))
115112, 114bitr2i 275 . . . . . . . . . . . . . 14 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ Fin) ↔ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
116111, 115sylib 217 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
117 ralnex 3075 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
118117imbi2i 335 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
119118albii 1821 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
120 alinexa 1845 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦(𝑣𝑦 → ¬ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)))
121119, 120bitr2i 275 . . . . . . . . . . . . . . . . . . . . 21 (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ↔ ∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)))
122 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 = 𝑧 → (𝑓𝑠) = (𝑓𝑧))
123122unieqd 4879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧 (𝑓𝑠) = (𝑓𝑧))
124 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 = 𝑧𝑠 = 𝑧)
125123, 124uneq12d 4124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = 𝑧 → ( (𝑓𝑠) ∪ 𝑠) = ( (𝑓𝑧) ∪ 𝑧))
126125eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = 𝑧 → (𝑋 = ( (𝑓𝑠) ∪ 𝑠) ↔ 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
127126rspcv 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → 𝑋 = ( (𝑓𝑧) ∪ 𝑧)))
128 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
129128biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧)))
130 elun 4108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (𝑣 (𝑓𝑧) ∨ 𝑣𝑧))
131 eluni 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 (𝑓𝑧) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
132131orbi1i 912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑣 (𝑓𝑧) ∨ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧))
133 df-or 846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
134 alinexa 1845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) ↔ ¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)))
135134imbi1i 349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) ↔ (¬ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
136133, 135bitr4i 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((∃𝑤(𝑣𝑤𝑤 ∈ (𝑓𝑧)) ∨ 𝑣𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
137130, 132, 1363bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧))
138 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑤 → (𝑣𝑦𝑣𝑤))
139 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑤 → (𝑦 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑠)))
140139notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑠)))
141140ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑤 → (∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠) ↔ ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
142138, 141imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑤 → ((𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) ↔ (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠))))
143142spvv 2000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠)))
144122eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 → (𝑤 ∈ (𝑓𝑠) ↔ 𝑤 ∈ (𝑓𝑧)))
145144notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓𝑠) ↔ ¬ 𝑤 ∈ (𝑓𝑧)))
146145rspcv 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧𝑡 → (∀𝑠𝑡 ¬ 𝑤 ∈ (𝑓𝑠) → ¬ 𝑤 ∈ (𝑓𝑧)))
147143, 146syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
148147alrimdv 1932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧))))
149148imim1d 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧𝑡 → ((∀𝑤(𝑣𝑤 → ¬ 𝑤 ∈ (𝑓𝑧)) → 𝑣𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
150137, 149biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
151150a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝑡 → (𝑣 ∈ ( (𝑓𝑧) ∪ 𝑧) → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧))))
152129, 151syl9r 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑡 → (𝑋 = ( (𝑓𝑧) ∪ 𝑧) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
153127, 152syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑤 = 𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
154153com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑡 → (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣𝑋 → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))))
155154imp31 418 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑧𝑡 → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑧)))
156155com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → (𝑧𝑡𝑣𝑧)))
157156ralrimdv 3149 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → ∀𝑧𝑡 𝑣𝑧))
158 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑣 ∈ V
159158elint2 4914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 𝑡 ↔ ∀𝑧𝑡 𝑣𝑧)
160157, 159syl6ibr 251 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣 𝑡))
161 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑡 → (𝑣𝑤𝑣 𝑡))
162161ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (𝑣𝑤𝑣 𝑡))
163160, 162sylibrd 258 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∀𝑦(𝑣𝑦 → ∀𝑠𝑡 ¬ 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
164121, 163biimtrid 241 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (¬ ∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → 𝑣𝑤))
165164orrd 861 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) ∧ 𝑣𝑋) → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤))
166165ex 413 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋 → (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤)))
167 orc 865 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
168167anim2i 617 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
169168eximi 1837 . . . . . . . . . . . . . . . . . . . 20 (∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
170 equid 2015 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 = 𝑤
171 vex 3449 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
172 equequ1 2028 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → (𝑦 = 𝑤𝑤 = 𝑤))
173138, 172anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑤 → ((𝑣𝑦𝑦 = 𝑤) ↔ (𝑣𝑤𝑤 = 𝑤)))
174171, 173spcev 3565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣𝑤𝑤 = 𝑤) → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
175170, 174mpan2 689 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑤 → ∃𝑦(𝑣𝑦𝑦 = 𝑤))
176 olc 866 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑤 → (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
177176anim2i 617 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣𝑦𝑦 = 𝑤) → (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
178177eximi 1837 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑦(𝑣𝑦𝑦 = 𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
179175, 178syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑤 → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
180169, 179jaoi 855 . . . . . . . . . . . . . . . . . . 19 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
181 eluni 4868 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
182 elun 4108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}))
183 eliun 4958 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠))
184 velsn 4602 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
185183, 184orbi12i 913 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 𝑠𝑡 (𝑓𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
186182, 185bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤))
187186anbi2i 623 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ (𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
188187exbii 1850 . . . . . . . . . . . . . . . . . . . 20 (∃𝑦(𝑣𝑦𝑦 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)))
189181, 188bitr2i 275 . . . . . . . . . . . . . . . . . . 19 (∃𝑦(𝑣𝑦 ∧ (∃𝑠𝑡 𝑦 ∈ (𝑓𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
190180, 189sylib 217 . . . . . . . . . . . . . . . . . 18 ((∃𝑦(𝑣𝑦 ∧ ∃𝑠𝑡 𝑦 ∈ (𝑓𝑠)) ∨ 𝑣𝑤) → 𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
191166, 190syl6 35 . . . . . . . . . . . . . . . . 17 ((𝑤 = 𝑡 ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
192191ad5ant25 760 . . . . . . . . . . . . . . . 16 (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
193192ad2ant2l 744 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣𝑋𝑣 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})))
194193ssrdv 3950 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
195 elun 4108 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}))
196 eliun 4958 . . . . . . . . . . . . . . . . . . 19 (𝑣 𝑠𝑡 (𝑓𝑠) ↔ ∃𝑠𝑡 𝑣 ∈ (𝑓𝑠))
197 velsn 4602 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
198196, 197orbi12i 913 . . . . . . . . . . . . . . . . . 18 ((𝑣 𝑠𝑡 (𝑓𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
199195, 198bitri 274 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ↔ (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤))
200 nfra1 3267 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)
201 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑠 𝑣𝑋
202 rsp 3230 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡𝑋 = ( (𝑓𝑠) ∪ 𝑠)))
203 eqimss2 4001 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋)
204 elssuni 4898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (𝑓𝑠) → 𝑣 (𝑓𝑠))
205 ssun3 4134 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (𝑓𝑠) → 𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠))
207 sstr 3952 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) ∧ ( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣𝑋)
208207expcom 414 . . . . . . . . . . . . . . . . . . . . . 22 (( (𝑓𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ ( (𝑓𝑠) ∪ 𝑠) → 𝑣𝑋))
209203, 206, 208syl2im 40 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
210202, 209syl6 35 . . . . . . . . . . . . . . . . . . . 20 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (𝑠𝑡 → (𝑣 ∈ (𝑓𝑠) → 𝑣𝑋)))
211200, 201, 210rexlimd 3249 . . . . . . . . . . . . . . . . . . 19 (∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
212211ad2antll 727 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) → 𝑣𝑋))
213 elpwi 4567 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
214213ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → 𝑢 ⊆ (fi‘𝑥))
215214ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
216215, 99sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
217 elssuni 4898 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (fi‘𝑥) → 𝑤 (fi‘𝑥))
218216, 217syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤 (fi‘𝑥))
21956, 57ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘(fi‘𝑥)) = (fi‘𝑥)
22059, 219eqtr2di 2793 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝐽)
221220, 66eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 = (topGen‘(fi‘𝑥)) → (fi‘𝑥) = 𝑋)
2222213ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (fi‘𝑥) = 𝑋)
223222ad3antrrr 728 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (fi‘𝑥) = 𝑋)
224218, 223sseqtrd 3984 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑤𝑋)
225 sseq1 3969 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑣𝑋𝑤𝑋))
226224, 225syl5ibrcom 246 . . . . . . . . . . . . . . . . . 18 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 = 𝑤𝑣𝑋))
227212, 226jaod 857 . . . . . . . . . . . . . . . . 17 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ((∃𝑠𝑡 𝑣 ∈ (𝑓𝑠) ∨ 𝑣 = 𝑤) → 𝑣𝑋))
228199, 227biimtrid 241 . . . . . . . . . . . . . . . 16 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → (𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑣𝑋))
229228ralrimiv 3142 . . . . . . . . . . . . . . 15 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
230 unissb 4900 . . . . . . . . . . . . . . 15 ( ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})𝑣𝑋)
231229, 230sylibr 233 . . . . . . . . . . . . . 14 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ⊆ 𝑋)
232194, 231eqssd 3961 . . . . . . . . . . . . 13 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
233 unieq 4876 . . . . . . . . . . . . . 14 (𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) → 𝑏 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}))
234233rspceeqv 3595 . . . . . . . . . . . . 13 ((( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ( 𝑠𝑡 (𝑓𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
235116, 232, 234syl2anc 584 . . . . . . . . . . . 12 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏)
236235ex 413 . . . . . . . . . . 11 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
237236exlimdv 1936 . . . . . . . . . 10 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠𝑡 𝑋 = ( (𝑓𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
23878, 88, 2373syld 60 . . . . . . . . 9 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
2394, 238biimtrid 241 . . . . . . . 8 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏))
240 dfrex2 3076 . . . . . . . 8 (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏)
241239, 240syl6ib 250 . . . . . . 7 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (¬ ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))
242241con4d 115 . . . . . 6 ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) ∧ 𝑤𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))
243242exp32 421 . . . . 5 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → (𝑤𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
244243com24 95 . . . 4 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))
245244exp32 421 . . 3 ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏 → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛))))))
246245imp45 430 . 2 (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) → (𝑤𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)))
247246imp31 418 1 (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = 𝑏))) ∧ 𝑤𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = 𝑡) ∧ (𝑦𝑤 ∧ ¬ 𝑦 (𝑥𝑢)))) → ∃𝑠𝑡𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = 𝑛)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  𝒫 cpw 4560  {csn 4586   cuni 4865   cint 4907   ciun 4954  wf 6492  cfv 6496  Fincfn 8883  ficfi 9346  topGenctg 17319  TopBasesctb 22295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-er 8648  df-en 8884  df-fin 8887  df-fi 9347  df-topgen 17325  df-bases 22296
This theorem is referenced by:  alexsubALTlem4  23401
  Copyright terms: Public domain W3C validator