Theorem topdifinffinlem 37370

Description: This is the core of the proof of topdifinffin 37371, 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 1914	. . . . 5 ⊢ Ⅎ𝑢 ¬ 𝐴 ∈ Fin
2		nfab1 2901	. . . . 5 ⊢ Ⅎ𝑢{𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
3		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑢𝑇
4		abid 2718	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦})
5		df-rex 3062	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
6	4, 5	bitri 275	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
7		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ {𝑦} = {𝑦}
8		vsnex 5409	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦} ∈ V
9		snelpwi 5423	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴)
10		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
11	9, 10	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = {𝑦} → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
12	11	imdistani 568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
13	12	anim2i 617	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14	13	3impb 1114	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15		3anass 1094	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
16	14, 15	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17		snfi 9062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑦} ∈ Fin
18		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
19	17, 18	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20		difinf 9326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴 ∖ 𝑥) ∈ Fin)
21	19, 20	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴 ∖ 𝑥) ∈ Fin)
22	21	orcd 873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
23	22	anim2i 617	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
24	23	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25	24	3impa 1109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
26	16, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27		topdifinf.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
28	27	reqabi 3444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
29	26, 28	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝑇)
30		eleq1 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
31	30	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
32	29, 31	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
33	32	sbcth 3785	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇))
34	8, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
35		sbcimg 3819	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
36	8, 35	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
37	34, 36	mpbi 230	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38		sbc3an 3835	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
39		sbcg 3843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
40	8, 39	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41	40	3anbi1i 1157	. . . . . . . . . . . . . . . . . 18 ⊢ (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
42		eqsbc1 3817	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
43	8, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44	43	3anbi2i 1158	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
45	38, 41, 44	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
46		sbcg 3843	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
47	8, 46	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
48	47	3anbi3i 1159	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
49	45, 48	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
50		sbcg 3843	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
51	8, 50	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
52	37, 49, 51	3imtr3i 291	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
53	7, 52	mp3an2 1451	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
54	53	ex 412	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑇))
55	54	pm4.71d 561	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇)))
56	55	anbi1d 631	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
57	56	exbidv 1921	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
58	6, 57	bitrid 283	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59		anass 468	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
60	59	exbii 1848	. . . . . . . . . 10 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
61		exsimpr 1869	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
62	60, 61	sylbi 217	. . . . . . . . 9 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
63	58, 62	biimtrdi 253	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
64		ancom 460	. . . . . . . . . 10 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65		eleq1 2823	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑦} → (𝑢 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
66	65	pm5.32i 574	. . . . . . . . . 10 ⊢ ((𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
67	64, 66	bitr4i 278	. . . . . . . . 9 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
68	67	exbii 1848	. . . . . . . 8 ⊢ (∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
69	63, 68	imbitrdi 251	. . . . . . 7 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇)))
70		exsimpr 1869	. . . . . . 7 ⊢ (∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) → ∃𝑦 𝑢 ∈ 𝑇)
71	69, 70	syl6 35	. . . . . 6 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢 ∈ 𝑇))
72		ax5e 1912	. . . . . 6 ⊢ (∃𝑦 𝑢 ∈ 𝑇 → 𝑢 ∈ 𝑇)
73	71, 72	syl6 35	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → 𝑢 ∈ 𝑇))
74	1, 2, 3, 73	ssrd 3968	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75		eqid 2736	. . . . 5 ⊢ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
76	75	dissneq 37364	. . . 4 ⊢ (({𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇 ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
77	74, 76	sylan 580	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78		nfielex 9284	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑦 𝑦 ∈ 𝐴)
79	78	adantr 480	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦 ∈ 𝐴)
80		difss 4116	. . . . . . 7 ⊢ (𝐴 ∖ {𝑦}) ⊆ 𝐴
81		elfvex 6919	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82		difexg 5304	. . . . . . . 8 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83		elpwg 4583	. . . . . . . 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 9326	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
88	17, 87	mpan2 691	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89		0fi 9061	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
90		eleq1 2823	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
91	89, 90	mpbiri 258	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
92	88, 91	nsyl 140	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
93	92	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94		vsnid 4644	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ {𝑦}
95		inelcm 4445	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
96	94, 95	mpan2 691	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97		disj4 4439	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
98	97	necon2abii 2983	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
99	96, 98	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
100	99	pssned 4081	. . . . . . . . . . 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 990	. . . . . . . 8 ⊢ ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105	103, 104	sylib 218	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106		difeq2 4100	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107	106	eleq1d 2820	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108	107	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109		eqeq1 2740	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110		eqeq1 2740	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111	109, 110	orbi12d 918	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112	108, 111	orbi12d 918	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113	112, 27	elrab2 3679	. . . . . . . . . 10 ⊢ ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
114	85	biantrurd 532	. . . . . . . . . 10 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115	113, 114	bitr4id 290	. . . . . . . . 9 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116		dfin4 4258	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117		inss2 4218	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118		ssfi 9192	. . . . . . . . . . . 12 ⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
119	17, 117, 118	mp2an 692	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) ∈ Fin
120	116, 119	eqeltrri 2832	. . . . . . . . . 10 ⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121		biortn 937	. . . . . . . . . 10 ⊢ ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122	120, 121	ax-mp 5	. . . . . . . . 9 ⊢ (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123	115, 122	bitr4di 289	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124	123	ad2antll 729	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125	105, 124	mtbird 325	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126	125	expcom 413	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127		nelneq2 2860	. . . . . 6 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128		eqcom 2743	. . . . . 6 ⊢ (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129	127, 128	sylnibr 329	. . . . 5 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
130	86, 126, 129	syl6an 684	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ 𝑇 = 𝒫 𝐴))
131	79, 130	exellimddv 37368	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
132	77, 131	pm2.65da 816	. 2 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133	132	con4i 114	1 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∃wrex 3061  {crab 3420  Vcvv 3464  [wsbc 3770   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931   ⊊ wpss 3932  ∅c0 4313  𝒫 cpw 4580  {csn 4606  ‘cfv 6536  Fincfn 8964  TopOnctopon 22853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7867  df-1o 8485  df-en 8965  df-fin 8968  df-topgen 17462  df-top 22837  df-topon 22854

This theorem is referenced by:  topdifinffin  37371