Theorem topdifinffinlem 37916

Description: This is the core of the proof of topdifinffin 37917, 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 1941	. . . . 5 ⊢ Ⅎ𝑢 ¬ 𝐴 ∈ Fin
2		nfab1 2933	. . . . 5 ⊢ Ⅎ𝑢{𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
3		nfcv 2931	. . . . 5 ⊢ Ⅎ𝑢𝑇
4		abid 2751	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦})
5		df-rex 3096	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
6	4, 5	bitri 278	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}))
7		eqid 2769	. . . . . . . . . . . . . . 15 ⊢ {𝑦} = {𝑦}
8		vsnex 5407	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦} ∈ V
9		snelpwi 5426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴)
10		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
11	9, 10	imbitrrid 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = {𝑦} → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
12	11	imdistani 578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
13	12	anim2i 628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14	13	3impb 1130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15		3anass 1109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
16	14, 15	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17		snfi 9040	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑦} ∈ Fin
18		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
19	17, 18	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20		difinf 9271	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
26	16, 25	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27		topdifinf.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
28	27	reqabi 3445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
29	26, 28	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝑇)
30		eleq1 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
31	30	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
32	29, 31	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
33	32	sbcth 3766	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇))
34	8, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
35		sbcimg 3799	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
36	8, 35	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
37	34, 36	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38		sbc3an 3815	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
39		sbcg 3823	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
40	8, 39	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41	40	3anbi1i 1173	. . . . . . . . . . . . . . . . . 18 ⊢ (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
42		eqsbc1 3797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
43	8, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44	43	3anbi2i 1174	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
45	38, 41, 44	3bitri 300	. . . . . . . . . . . . . . . . 17 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴))
46		sbcg 3823	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
47	8, 46	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
48	47	3anbi3i 1175	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
49	45, 48	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
50		sbcg 3823	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
51	8, 50	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
52	37, 49, 51	3imtr3i 294	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
53	7, 52	mp3an2 1475	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)
54	53	ex 417	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑇))
55	54	pm4.71d 570	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ Fin → (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇)))
56	55	anbi1d 642	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
57	56	exbidv 1948	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
58	6, 57	bitrid 286	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59		anass 473	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
60	59	exbii 1875	. . . . . . . . . 10 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
61		exsimpr 1896	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
62	60, 61	sylbi 220	. . . . . . . . 9 ⊢ (∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))
63	58, 62	biimtrdi 256	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})))
64		ancom 465	. . . . . . . . . 10 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65		eleq1 2857	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑦} → (𝑢 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
66	65	pm5.32i 584	. . . . . . . . . 10 ⊢ ((𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
67	64, 66	bitr4i 281	. . . . . . . . 9 ⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
68	67	exbii 1875	. . . . . . . 8 ⊢ (∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))
69	63, 68	imbitrdi 254	. . . . . . 7 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇)))
70		exsimpr 1896	. . . . . . 7 ⊢ (∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) → ∃𝑦 𝑢 ∈ 𝑇)
71	69, 70	syl6 36	. . . . . 6 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢 ∈ 𝑇))
72		ax5e 1939	. . . . . 6 ⊢ (∃𝑦 𝑢 ∈ 𝑇 → 𝑢 ∈ 𝑇)
73	71, 72	syl6 36	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → 𝑢 ∈ 𝑇))
74	1, 2, 3, 73	ssrd 3948	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75		eqid 2769	. . . . 5 ⊢ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}}
76	75	dissneq 37910	. . . 4 ⊢ (({𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇 ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
77	74, 76	sylan 591	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78		nfielex 9234	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑦 𝑦 ∈ 𝐴)
79	78	adantr 485	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦 ∈ 𝐴)
80		difss 4096	. . . . . . 7 ⊢ (𝐴 ∖ {𝑦}) ⊆ 𝐴
81		elfvex 6917	. . . . . . . 8 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82		difexg 5300	. . . . . . . 8 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83		elpwg 4568	. . . . . . . 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 9271	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
88	17, 87	mpan2 703	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89		0fi 9039	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
90		eleq1 2857	. . . . . . . . . . . 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 4632	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ {𝑦}
95		inelcm 4429	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
96	94, 95	mpan2 703	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97		disj4 4423	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
98	97	necon2abii 3014	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
99	96, 98	sylibr 237	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
100	99	pssned 4061	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101	100	adantr 485	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102	101	neneqd 2969	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
103	93, 102	jca 520	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104		pm4.56 1004	. . . . . . . 8 ⊢ ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105	103, 104	sylib 221	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106		difeq2 4081	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107	106	eleq1d 2854	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108	107	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109		eqeq1 2773	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110		eqeq1 2773	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111	109, 110	orbi12d 931	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112	108, 111	orbi12d 931	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113	112, 27	elrab2 3661	. . . . . . . . . 10 ⊢ ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
114	85	biantrurd 541	. . . . . . . . . 10 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115	113, 114	bitr4id 293	. . . . . . . . 9 ⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116		dfin4 4237	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117		inss2 4196	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118		ssfi 9157	. . . . . . . . . . . 12 ⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
119	17, 117, 118	mp2an 704	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {𝑦}) ∈ Fin
120	116, 119	eqeltrri 2866	. . . . . . . . . 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 2894	. . . . . 6 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128		eqcom 2776	. . . . . 6 ⊢ (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129	127, 128	sylnibr 332	. . . . 5 ⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
130	86, 126, 129	syl6an 696	. . . 4 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ 𝑇 = 𝒫 𝐴))
131	79, 130	exellimddv 37914	. . 3 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
132	77, 131	pm2.65da 828	. 2 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133	132	con4i 115	1 ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1567  ∃wex 1806   ∈ wcel 2149  {cab 2747   ≠ wne 2964  ∃wrex 3095  {crab 3422  Vcvv 3461  [wsbc 3751   ∖ cdif 3908   ∩ cin 3910   ⊆ wss 3911   ⊊ wpss 3912  ∅c0 4292  𝒫 cpw 4565  {csn 4592  ‘cfv 6537  Fincfn 8943  TopOnctopon 23036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7863  df-1o 8453  df-en 8944  df-fin 8947  df-topgen 17496  df-top 23020  df-topon 23037

This theorem is referenced by:  topdifinffin  37917