Theorem topdifinffinlem 37629

Description: This is the core of the proof of topdifinffin 37630, 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 1916	. . . . 5 ⊢ Ⅎ𝑢 ¬ 𝐴 ∈ Fin
2		nfab1 2901	. . . . 5 ⊢ Ⅎ𝑢{𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
3		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑢𝑇
4		abid 2719	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦})
5		df-rex 3063	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
6	4, 5	bitri 275	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
7		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ {𝑦} = {𝑦}
8		vsnex 5383	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦} ∈ V
9		snelpwi 5401	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴)
10		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
11	9, 10	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = {𝑦} → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
12	11	imdistani 568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
13	12	anim2i 618	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14	13	3impb 1115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15		3anass 1095	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
16	14, 15	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17		snfi 8994	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑦} ∈ Fin
18		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
19	17, 18	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20		difinf 9225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴 ∖ 𝑥) ∈ Fin)
21	19, 20	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴 ∖ 𝑥) ∈ Fin)
22	21	orcd 874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
23	22	anim2i 618	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
24	23	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25	24	3impa 1110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
26	16, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27		topdifinf.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
28	27	reqabi 3424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
29	26, 28	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝑇)
30		eleq1 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
31	30	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
32	29, 31	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
33	32	sbcth 3757	. . . . . . . . . . . . . . . . . 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 230	. . . . . . . . . . . . . . . 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 1158	. . . . . . . . . . . . . . . . . 18 ⊢ (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
42		eqsbc1 3789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
43	8, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44	43	3anbi2i 1159	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
45	38, 41, 44	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
46		sbcg 3815	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
47	8, 46	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
48	47	3anbi3i 1160	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
49	45, 48	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
50		sbcg 3815	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
51	8, 50	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
52	37, 49, 51	3imtr3i 291	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
53	7, 52	mp3an2 1452	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
54	53	ex 412	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑇))
55	54	pm4.71d 561	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇)))
56	55	anbi1d 632	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
57	56	exbidv 1923	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
58	6, 57	bitrid 283	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59		anass 468	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
60	59	exbii 1850	. . . . . . . . . 10 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
61		exsimpr 1871	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
62	60, 61	sylbi 217	. . . . . . . . 9 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
63	58, 62	biimtrdi 253	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
64		ancom 460	. . . . . . . . . 10 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65		eleq1 2825	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑦} → (𝑢 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
66	65	pm5.32i 574	. . . . . . . . . 10 ⊢ ((𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
67	64, 66	bitr4i 278	. . . . . . . . 9 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
68	67	exbii 1850	. . . . . . . 8 ⊢ (∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
69	63, 68	imbitrdi 251	. . . . . . 7 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇)))
70		exsimpr 1871	. . . . . . 7 ⊢ (∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) → ∃𝑦 𝑢 ∈ 𝑇)
71	69, 70	syl6 35	. . . . . 6 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢 ∈ 𝑇))
72		ax5e 1914	. . . . . 6 ⊢ (∃𝑦 𝑢 ∈ 𝑇 → 𝑢 ∈ 𝑇)
73	71, 72	syl6 35	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → 𝑢 ∈ 𝑇))
74	1, 2, 3, 73	ssrd 3940	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75		eqid 2737	. . . . 5 ⊢ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
76	75	dissneq 37623	. . . 4 ⊢ (({𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇 ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
77	74, 76	sylan 581	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78		nfielex 9188	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑦 𝑦 ∈ 𝐴)
79	78	adantr 480	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦 ∈ 𝐴)
80		difss 4090	. . . . . . 7 ⊢ (𝐴 ∖ {𝑦}) ⊆ 𝐴
81		elfvex 6879	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82		difexg 5278	. . . . . . . 8 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83		elpwg 4559	. . . . . . . 8 ⊢ ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
84	81, 82, 83	3syl 18	. . . . . . 7 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
85	80, 84	mpbiri 258	. . . . . 6 ⊢ (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
86	85	adantl 481	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87		difinf 9225	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
88	17, 87	mpan2 692	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89		0fi 8993	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
90		eleq1 2825	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
91	89, 90	mpbiri 258	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
92	88, 91	nsyl 140	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
93	92	ad2antrl 729	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94		vsnid 4622	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ {𝑦}
95		inelcm 4419	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
96	94, 95	mpan2 692	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97		disj4 4413	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
98	97	necon2abii 2983	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
99	96, 98	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
100	99	pssned 4055	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101	100	adantr 480	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102	101	neneqd 2938	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
103	93, 102	jca 511	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104		pm4.56 991	. . . . . . . 8 ⊢ ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105	103, 104	sylib 218	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106		difeq2 4074	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107	106	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108	107	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109		eqeq1 2741	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110		eqeq1 2741	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111	109, 110	orbi12d 919	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112	108, 111	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113	112, 27	elrab2 3651	. . . . . . . . . 10 ⊢ ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
114	85	biantrurd 532	. . . . . . . . . 10 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115	113, 114	bitr4id 290	. . . . . . . . 9 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116		dfin4 4232	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117		inss2 4192	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118		ssfi 9111	. . . . . . . . . . . 12 ⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
119	17, 117, 118	mp2an 693	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) ∈ Fin
120	116, 119	eqeltrri 2834	. . . . . . . . . 10 ⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121		biortn 938	. . . . . . . . . 10 ⊢ ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122	120, 121	ax-mp 5	. . . . . . . . 9 ⊢ (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123	115, 122	bitr4di 289	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124	123	ad2antll 730	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125	105, 124	mtbird 325	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126	125	expcom 413	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127		nelneq2 2862	. . . . . 6 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128		eqcom 2744	. . . . . 6 ⊢ (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129	127, 128	sylnibr 329	. . . . 5 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
130	86, 126, 129	syl6an 685	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ 𝑇 = 𝒫 𝐴))
131	79, 130	exellimddv 37627	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
132	77, 131	pm2.65da 817	. 2 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133	132	con4i 114	1 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∃wrex 3062  {crab 3401  Vcvv 3442  [wsbc 3742   ∖ cdif 3900   ∩ cin 3902   ⊆ wss 3903   ⊊ wpss 3904  ∅c0 4287  𝒫 cpw 4556  {csn 4582  ‘cfv 6502  Fincfn 8897  TopOnctopon 22871

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-om 7821  df-1o 8409  df-en 8898  df-fin 8901  df-topgen 17377  df-top 22855  df-topon 22872

This theorem is referenced by:  topdifinffin  37630