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 
|- T = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
Assertion topdifinffinlem 
|- ( T e. ( TopOn ` A ) -> A e. Fin )

Proof

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