Metamath Proof Explorer

Theorem topdifinffinlem

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

Ref Expression
Hypothesis topdifinf.t ⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
Assertion topdifinffinlem ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ Fin )

Proof

Step Hyp Ref Expression
1 topdifinf.t ⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
2 nfv ⊢ Ⅎ 𝑢 ¬ 𝐴 ∈ Fin
3 nfab1 ⊢ Ⅎ 𝑢 { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } }
4 nfcv ⊢ Ⅎ 𝑢 𝑇
5 abid ⊢ ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } ↔ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } )
6 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑢 = { 𝑦 } ) )
7 5 6 bitri ⊢ ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑢 = { 𝑦 } ) )
8 eqid ⊢ { 𝑦 } = { 𝑦 }
9 snex ⊢ { 𝑦 } ∈ V
10 snelpwi ⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ∈ 𝒫 𝐴 )
11 eleq1 ⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ∈ 𝒫 𝐴 ↔ { 𝑦 } ∈ 𝒫 𝐴 ) )
12 10 11 syl5ibr ⊢ ( 𝑥 = { 𝑦 } → ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
13 12 imdistani ⊢ ( ( 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) )
14 13 anim2i ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) ) )
15 14 3impb ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) ) )
16 3anass ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) ↔ ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) ) )
17 15 16 sylibr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) )
18 snfi ⊢ { 𝑦 } ∈ Fin
19 eleq1 ⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ∈ Fin ↔ { 𝑦 } ∈ Fin ) )
20 18 19 mpbiri ⊢ ( 𝑥 = { 𝑦 } → 𝑥 ∈ Fin )
21 difinf ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin )
22 20 21 sylan2 ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin )
23 22 orcd ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ) → ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) )
24 23 anim2i ⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ) ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
25 24 ancoms ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ) ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
26 25 3impa ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
27 17 26 syl ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
28 1 rabeq2i ⊢ ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
29 27 28 sylibr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝑇 )
30 eleq1 ⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ∈ 𝑇 ↔ { 𝑦 } ∈ 𝑇 ) )
31 30 3ad2ant2 ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑇 ↔ { 𝑦 } ∈ 𝑇 ) )
32 29 31 mpbid ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 )
33 32 sbcth ⊢ ( { 𝑦 } ∈ V → [ { 𝑦 } / 𝑥 ] ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 ) )
34 9 33 ax-mp ⊢ [ { 𝑦 } / 𝑥 ] ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 )
35 sbcimg ⊢ ( { 𝑦 } ∈ V → ( [ { 𝑦 } / 𝑥 ] ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 ) ↔ ( [ { 𝑦 } / 𝑥 ] ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → [ { 𝑦 } / 𝑥 ] { 𝑦 } ∈ 𝑇 ) ) )
36 9 35 ax-mp ⊢ ( [ { 𝑦 } / 𝑥 ] ( ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 ) ↔ ( [ { 𝑦 } / 𝑥 ] ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → [ { 𝑦 } / 𝑥 ] { 𝑦 } ∈ 𝑇 ) )
37 34 36 mpbi ⊢ ( [ { 𝑦 } / 𝑥 ] ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → [ { 𝑦 } / 𝑥 ] { 𝑦 } ∈ 𝑇 )
38 sbc3an ⊢ ( [ { 𝑦 } / 𝑥 ] ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) ↔ ( [ { 𝑦 } / 𝑥 ] ¬ 𝐴 ∈ Fin ∧ [ { 𝑦 } / 𝑥 ] 𝑥 = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) )
39 sbcg ⊢ ( { 𝑦 } ∈ V → ( [ { 𝑦 } / 𝑥 ] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin ) )
40 9 39 ax-mp ⊢ ( [ { 𝑦 } / 𝑥 ] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin )
41 40 3anbi1i ⊢ ( ( [ { 𝑦 } / 𝑥 ] ¬ 𝐴 ∈ Fin ∧ [ { 𝑦 } / 𝑥 ] 𝑥 = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) ↔ ( ¬ 𝐴 ∈ Fin ∧ [ { 𝑦 } / 𝑥 ] 𝑥 = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) )
42 eqsbc1 ⊢ ( { 𝑦 } ∈ V → ( [ { 𝑦 } / 𝑥 ] 𝑥 = { 𝑦 } ↔ { 𝑦 } = { 𝑦 } ) )
43 9 42 ax-mp ⊢ ( [ { 𝑦 } / 𝑥 ] 𝑥 = { 𝑦 } ↔ { 𝑦 } = { 𝑦 } )
44 43 3anbi2i ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ [ { 𝑦 } / 𝑥 ] 𝑥 = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) ↔ ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) )
45 38 41 44 3bitri ⊢ ( [ { 𝑦 } / 𝑥 ] ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) ↔ ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) )
46 sbcg ⊢ ( { 𝑦 } ∈ V → ( [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
47 9 46 ax-mp ⊢ ( [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
48 47 3anbi3i ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } = { 𝑦 } ∧ [ { 𝑦 } / 𝑥 ] 𝑦 ∈ 𝐴 ) ↔ ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) )
49 45 48 bitri ⊢ ( [ { 𝑦 } / 𝑥 ] ( ¬ 𝐴 ∈ Fin ∧ 𝑥 = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) ↔ ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) )
50 sbcg ⊢ ( { 𝑦 } ∈ V → ( [ { 𝑦 } / 𝑥 ] { 𝑦 } ∈ 𝑇 ↔ { 𝑦 } ∈ 𝑇 ) )
51 9 50 ax-mp ⊢ ( [ { 𝑦 } / 𝑥 ] { 𝑦 } ∈ 𝑇 ↔ { 𝑦 } ∈ 𝑇 )
52 37 49 51 3imtr3i ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } = { 𝑦 } ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 )
53 8 52 mp3an2 ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴 ) → { 𝑦 } ∈ 𝑇 )
54 53 ex ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑦 ∈ 𝐴 → { 𝑦 } ∈ 𝑇 ) )
55 54 pm4.71d ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ) )
56 55 anbi1d ⊢ ( ¬ 𝐴 ∈ Fin → ( ( 𝑦 ∈ 𝐴 ∧ 𝑢 = { 𝑦 } ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ∧ 𝑢 = { 𝑦 } ) ) )
57 56 exbidv ⊢ ( ¬ 𝐴 ∈ Fin → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑢 = { 𝑦 } ) ↔ ∃ 𝑦 ( ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ∧ 𝑢 = { 𝑦 } ) ) )
58 7 57 syl5bb ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } ↔ ∃ 𝑦 ( ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ∧ 𝑢 = { 𝑦 } ) ) )
59 anass ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ∧ 𝑢 = { 𝑦 } ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ) )
60 59 exbii ⊢ ( ∃ 𝑦 ( ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ∧ 𝑢 = { 𝑦 } ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ) )
61 exsimpr ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ) → ∃ 𝑦 ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) )
62 60 61 sylbi ⊢ ( ∃ 𝑦 ( ( 𝑦 ∈ 𝐴 ∧ { 𝑦 } ∈ 𝑇 ) ∧ 𝑢 = { 𝑦 } ) → ∃ 𝑦 ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) )
63 58 62 syl6bi ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } → ∃ 𝑦 ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ) )
64 ancom ⊢ ( ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ↔ ( 𝑢 = { 𝑦 } ∧ { 𝑦 } ∈ 𝑇 ) )
65 eleq1 ⊢ ( 𝑢 = { 𝑦 } → ( 𝑢 ∈ 𝑇 ↔ { 𝑦 } ∈ 𝑇 ) )
66 65 pm5.32i ⊢ ( ( 𝑢 = { 𝑦 } ∧ 𝑢 ∈ 𝑇 ) ↔ ( 𝑢 = { 𝑦 } ∧ { 𝑦 } ∈ 𝑇 ) )
67 64 66 bitr4i ⊢ ( ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ↔ ( 𝑢 = { 𝑦 } ∧ 𝑢 ∈ 𝑇 ) )
68 67 exbii ⊢ ( ∃ 𝑦 ( { 𝑦 } ∈ 𝑇 ∧ 𝑢 = { 𝑦 } ) ↔ ∃ 𝑦 ( 𝑢 = { 𝑦 } ∧ 𝑢 ∈ 𝑇 ) )
69 63 68 syl6ib ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } → ∃ 𝑦 ( 𝑢 = { 𝑦 } ∧ 𝑢 ∈ 𝑇 ) ) )
70 exsimpr ⊢ ( ∃ 𝑦 ( 𝑢 = { 𝑦 } ∧ 𝑢 ∈ 𝑇 ) → ∃ 𝑦 𝑢 ∈ 𝑇 )
71 69 70 syl6 ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } → ∃ 𝑦 𝑢 ∈ 𝑇 ) )
72 ax5e ⊢ ( ∃ 𝑦 𝑢 ∈ 𝑇 → 𝑢 ∈ 𝑇 )
73 71 72 syl6 ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } → 𝑢 ∈ 𝑇 ) )
74 2 3 4 73 ssrd ⊢ ( ¬ 𝐴 ∈ Fin → { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } ⊆ 𝑇 )
75 eqid ⊢ { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } = { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } }
76 75 dissneq ⊢ ( ( { 𝑢 ∣ ∃ 𝑦 ∈ 𝐴 𝑢 = { 𝑦 } } ⊆ 𝑇 ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → 𝑇 = 𝒫 𝐴 )
77 74 76 sylan ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → 𝑇 = 𝒫 𝐴 )
78 nfielex ⊢ ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 𝑦 ∈ 𝐴 )
79 78 adantr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → ∃ 𝑦 𝑦 ∈ 𝐴 )
80 difss ⊢ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴
81 elfvex ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ V )
82 difexg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ { 𝑦 } ) ∈ V )
83 elpwg ⊢ ( ( 𝐴 ∖ { 𝑦 } ) ∈ V → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴 ) )
84 81 82 83 3syl ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝐴 ) )
85 80 84 mpbiri ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 )
86 85 adantl ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 )
87 difinf ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ { 𝑦 } ∈ Fin ) → ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ Fin )
88 18 87 mpan2 ⊢ ( ¬ 𝐴 ∈ Fin → ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ Fin )
89 0fin ⊢ ∅ ∈ Fin
90 eleq1 ⊢ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ → ( ( 𝐴 ∖ { 𝑦 } ) ∈ Fin ↔ ∅ ∈ Fin ) )
91 89 90 mpbiri ⊢ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ → ( 𝐴 ∖ { 𝑦 } ) ∈ Fin )
92 88 91 nsyl ⊢ ( ¬ 𝐴 ∈ Fin → ¬ ( 𝐴 ∖ { 𝑦 } ) = ∅ )
93 92 ad2antrl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ¬ ( 𝐴 ∖ { 𝑦 } ) = ∅ )
94 vsnid ⊢ 𝑦 ∈ { 𝑦 }
95 inelcm ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑦 } ) → ( 𝐴 ∩ { 𝑦 } ) ≠ ∅ )
96 94 95 mpan2 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐴 ∩ { 𝑦 } ) ≠ ∅ )
97 disj4 ⊢ ( ( 𝐴 ∩ { 𝑦 } ) = ∅ ↔ ¬ ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 )
98 97 necon2abii ⊢ ( ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ↔ ( 𝐴 ∩ { 𝑦 } ) ≠ ∅ )
99 96 98 sylibr ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 )
100 99 pssned ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ≠ 𝐴 )
101 100 adantr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ( 𝐴 ∖ { 𝑦 } ) ≠ 𝐴 )
102 101 neneqd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ¬ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 )
103 93 102 jca ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ( ¬ ( 𝐴 ∖ { 𝑦 } ) = ∅ ∧ ¬ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) )
104 pm4.56 ⊢ ( ( ¬ ( 𝐴 ∖ { 𝑦 } ) = ∅ ∧ ¬ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ↔ ¬ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) )
105 103 104 sylib ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ¬ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) )
106 difeq2 ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) )
107 106 eleq1d ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ) )
108 107 notbid ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ) )
109 eqeq1 ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝑥 = ∅ ↔ ( 𝐴 ∖ { 𝑦 } ) = ∅ ) )
110 eqeq1 ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝑥 = 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) )
111 109 110 orbi12d ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) )
112 108 111 orbi12d ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ↔ ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) ) )
113 112 1 elrab2 ⊢ ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ↔ ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) ) )
114 85 biantrurd ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → ( ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) ↔ ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) ) ) )
115 113 114 bitr4id ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ↔ ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) ) )
116 dfin4 ⊢ ( 𝐴 ∩ { 𝑦 } ) = ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) )
117 inss2 ⊢ ( 𝐴 ∩ { 𝑦 } ) ⊆ { 𝑦 }
118 ssfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ ( 𝐴 ∩ { 𝑦 } ) ⊆ { 𝑦 } ) → ( 𝐴 ∩ { 𝑦 } ) ∈ Fin )
119 18 117 118 mp2an ⊢ ( 𝐴 ∩ { 𝑦 } ) ∈ Fin
120 116 119 eqeltrri ⊢ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin
121 biortn ⊢ ( ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin → ( ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ↔ ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) ) )
122 120 121 ax-mp ⊢ ( ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ↔ ( ¬ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ∨ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) )
123 115 122 bitr4di ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ↔ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) )
124 123 ad2antll ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ↔ ( ( 𝐴 ∖ { 𝑦 } ) = ∅ ∨ ( 𝐴 ∖ { 𝑦 } ) = 𝐴 ) ) )
125 105 124 mtbird ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) ) → ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 )
126 125 expcom ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ) )
127 nelneq2 ⊢ ( ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 ∧ ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ) → ¬ 𝒫 𝐴 = 𝑇 )
128 eqcom ⊢ ( 𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇 )
129 127 128 sylnibr ⊢ ( ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝐴 ∧ ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ 𝑇 ) → ¬ 𝑇 = 𝒫 𝐴 )
130 86 126 129 syl6an ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → ( 𝑦 ∈ 𝐴 → ¬ 𝑇 = 𝒫 𝐴 ) )
131 79 130 exellimddv ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) → ¬ 𝑇 = 𝒫 𝐴 )
132 77 131 pm2.65da ⊢ ( ¬ 𝐴 ∈ Fin → ¬ 𝑇 ∈ ( TopOn ‘ 𝐴 ) )
133 132 con4i ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ Fin )