This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-locfin

Description: Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Assertion df-locfin LocFin = ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clocfin ⊢ LocFin
1 vx ⊢ 𝑥
2 ctop ⊢ Top
3 vy ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 4 cuni ⊢ ∪ 𝑥
6 3 cv ⊢ 𝑦
7 6 cuni ⊢ ∪ 𝑦
8 5 7 wceq ⊢ ∪ 𝑥 = ∪ 𝑦
9 vp ⊢ 𝑝
10 vn ⊢ 𝑛
11 9 cv ⊢ 𝑝
12 10 cv ⊢ 𝑛
13 11 12 wcel ⊢ 𝑝 ∈ 𝑛
14 vs ⊢ 𝑠
15 14 cv ⊢ 𝑠
16 15 12 cin ⊢ ( 𝑠 ∩ 𝑛 )
17 c0 ⊢ ∅
18 16 17 wne ⊢ ( 𝑠 ∩ 𝑛 ) ≠ ∅
19 18 14 6 crab ⊢ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ }
20 cfn ⊢ Fin
21 19 20 wcel ⊢ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin
22 13 21 wa ⊢ ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
23 22 10 4 wrex ⊢ ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
24 23 9 5 wral ⊢ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
25 8 24 wa ⊢ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
26 25 3 cab ⊢ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) }
27 1 2 26 cmpt ⊢ ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )
28 0 27 wceq ⊢ LocFin = ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )