Theorem topdifinffinlem 38021

Description: This is the core of the proof of topdifinffin 38022, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.)

Hypothesis

Ref	Expression
topdifinf.t	⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}

Assertion

Ref	Expression
topdifinffinlem	⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑇

Proof of Theorem topdifinffinlem

Dummy variables 𝑢 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1943	. . . . 5 ⊢ Ⅎ𝑢 ¬ 𝐴 ∈ Fin
2		nfab1 2926	. . . . 5 ⊢ Ⅎ𝑢{𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
3		nfcv 2924	. . . . 5 ⊢ Ⅎ𝑢𝑇
4		abid 2744	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦})
5		df-rex 3089	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
6	4, 5	bitri 278	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
7		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ {𝑦} = {𝑦}
8		vsnex 5405	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦} ∈ V
9		snelpwi 5424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴)
10		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
11	9, 10	imbitrrid 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = {𝑦} → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
12	11	imdistani 578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
13	12	anim2i 628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14	13	3impb 1131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15		3anass 1110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
16	14, 15	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17		snfi 9038	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑦} ∈ Fin
18		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
19	17, 18	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20		difinf 9269	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴 ∖ 𝑥) ∈ Fin)
21	19, 20	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴 ∖ 𝑥) ∈ Fin)
22	21	orcd 886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
23	22	anim2i 628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
24	23	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25	24	3impa 1126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
26	16, 25	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27		topdifinf.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
28	27	reqabi 3438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
29	26, 28	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝑇)
30		eleq1 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
31	30	3ad2ant2 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
32	29, 31	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
33	32	sbcth 3758	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇))
34	8, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
35		sbcimg 3791	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
36	8, 35	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
37	34, 36	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38		sbc3an 3807	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
39		sbcg 3815	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
40	8, 39	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41	40	3anbi1i 1174	. . . . . . . . . . . . . . . . . 18 ⊢ (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
42		eqsbc1 3789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
43	8, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44	43	3anbi2i 1175	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
45	38, 41, 44	3bitri 300	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
46		sbcg 3815	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
47	8, 46	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
48	47	3anbi3i 1176	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
49	45, 48	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
50		sbcg 3815	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
51	8, 50	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
52	37, 49, 51	3imtr3i 294	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
53	7, 52	mp3an2 1477	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
54	53	ex 417	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑇))
55	54	pm4.71d 570	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇)))
56	55	anbi1d 642	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
57	56	exbidv 1950	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
58	6, 57	bitrid 286	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59		anass 473	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
60	59	exbii 1877	. . . . . . . . . 10 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
61		exsimpr 1898	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
62	60, 61	sylbi 220	. . . . . . . . 9 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
63	58, 62	biimtrdi 256	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
64		ancom 465	. . . . . . . . . 10 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65		eleq1 2850	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑦} → (𝑢 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
66	65	pm5.32i 584	. . . . . . . . . 10 ⊢ ((𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
67	64, 66	bitr4i 281	. . . . . . . . 9 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
68	67	exbii 1877	. . . . . . . 8 ⊢ (∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
69	63, 68	imbitrdi 254	. . . . . . 7 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇)))
70		exsimpr 1898	. . . . . . 7 ⊢ (∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) → ∃𝑦 𝑢 ∈ 𝑇)
71	69, 70	syl6 36	. . . . . 6 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢 ∈ 𝑇))
72		ax5e 1941	. . . . . 6 ⊢ (∃𝑦 𝑢 ∈ 𝑇 → 𝑢 ∈ 𝑇)
73	71, 72	syl6 36	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → 𝑢 ∈ 𝑇))
74	1, 2, 3, 73	ssrd 3941	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75		eqid 2762	. . . . 5 ⊢ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
76	75	dissneq 38015	. . . 4 ⊢ (({𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇 ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
77	74, 76	sylan 591	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78		nfielex 9232	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑦 𝑦 ∈ 𝐴)
79	78	adantr 485	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦 ∈ 𝐴)
80		difss 4089	. . . . . . 7 ⊢ (𝐴 ∖ {𝑦}) ⊆ 𝐴
81		elfvex 6916	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82		difexg 5299	. . . . . . . 8 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83		elpwg 4564	. . . . . . . 8 ⊢ ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
84	81, 82, 83	3syl 19	. . . . . . 7 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
85	80, 84	mpbiri 261	. . . . . 6 ⊢ (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
86	85	adantl 486	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87		difinf 9269	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
88	17, 87	mpan2 703	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89		0fi 9037	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
90		eleq1 2850	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
91	89, 90	mpbiri 261	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
92	88, 91	nsyl 141	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
93	92	ad2antrl 740	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94		vsnid 4628	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ {𝑦}
95		inelcm 4424	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
96	94, 95	mpan2 703	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97		disj4 4418	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
98	97	necon2abii 3007	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
99	96, 98	sylibr 237	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
100	99	pssned 4054	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101	100	adantr 485	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102	101	neneqd 2962	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
103	93, 102	jca 520	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104		pm4.56 1003	. . . . . . . 8 ⊢ ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105	103, 104	sylib 221	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106		difeq2 4074	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107	106	eleq1d 2847	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108	107	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109		eqeq1 2766	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110		eqeq1 2766	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111	109, 110	orbi12d 931	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112	108, 111	orbi12d 931	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113	112, 27	elrab2 3653	. . . . . . . . . 10 ⊢ ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
114	85	biantrurd 541	. . . . . . . . . 10 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115	113, 114	bitr4id 293	. . . . . . . . 9 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116		dfin4 4230	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117		inss2 4189	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118		ssfi 9155	. . . . . . . . . . . 12 ⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
119	17, 117, 118	mp2an 704	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) ∈ Fin
120	116, 119	eqeltrri 2859	. . . . . . . . . 10 ⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121		biortn 950	. . . . . . . . . 10 ⊢ ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122	120, 121	ax-mp 5	. . . . . . . . 9 ⊢ (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123	115, 122	bitr4di 292	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124	123	ad2antll 741	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125	105, 124	mtbird 328	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126	125	expcom 418	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127		nelneq2 2887	. . . . . 6 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128		eqcom 2769	. . . . . 6 ⊢ (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129	127, 128	sylnibr 332	. . . . 5 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
130	86, 126, 129	syl6an 696	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ 𝑇 = 𝒫 𝐴))
131	79, 130	exellimddv 38019	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
132	77, 131	pm2.65da 828	. 2 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133	132	con4i 115	1 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1102   = wceq 1569  ∃wex 1808   ∈ wcel 2142  {cab 2740   ≠ wne 2957  ∃wrex 3088  {crab 3415  Vcvv 3454  [wsbc 3743   ∖ cdif 3901   ∩ cin 3903   ⊆ wss 3904   ⊊ wpss 3905  ∅c0 4285  𝒫 cpw 4561  {csn 4588  ‘cfv 6536  Fincfn 8941  TopOnctopon 23078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7861  df-1o 8451  df-en 8942  df-fin 8945  df-topgen 17502  df-top 23062  df-topon 23079

This theorem is used by:  topdifinffin  38022