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

Metamath Proof Explorer

Theorem islocfin

Description: The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Hypotheses islocfin.1 ⊢ 𝑋 = ∪ 𝐽
islocfin.2 ⊢ 𝑌 = ∪ 𝐴
Assertion islocfin ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 islocfin.1 ⊢ 𝑋 = ∪ 𝐽
2 islocfin.2 ⊢ 𝑌 = ∪ 𝐴
3 df-locfin ⊢ LocFin = ( 𝑗 ∈ Top ↦ { 𝑦 ∣ ( ∪ 𝑗 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑛 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )
4 3 mptrcl ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝐽 ∈ Top )
5 eqimss2 ⊢ ( 𝑋 = ∪ 𝑦 → ∪ 𝑦 ⊆ 𝑋 )
6 sspwuni ⊢ ( 𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 )
7 5 6 sylibr ⊢ ( 𝑋 = ∪ 𝑦 → 𝑦 ⊆ 𝒫 𝑋 )
8 velpw ⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 ↔ 𝑦 ⊆ 𝒫 𝑋 )
9 7 8 sylibr ⊢ ( 𝑋 = ∪ 𝑦 → 𝑦 ∈ 𝒫 𝒫 𝑋 )
10 9 adantr ⊢ ( ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) → 𝑦 ∈ 𝒫 𝒫 𝑋 )
11 10 abssi ⊢ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ⊆ 𝒫 𝒫 𝑋
12 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
13 pwexg ⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V )
14 pwexg ⊢ ( 𝒫 𝑋 ∈ V → 𝒫 𝒫 𝑋 ∈ V )
15 12 13 14 3syl ⊢ ( 𝐽 ∈ Top → 𝒫 𝒫 𝑋 ∈ V )
16 ssexg ⊢ ( ( { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ⊆ 𝒫 𝒫 𝑋 ∧ 𝒫 𝒫 𝑋 ∈ V ) → { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ∈ V )
17 11 15 16 sylancr ⊢ ( 𝐽 ∈ Top → { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ∈ V )
18 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
19 18 1 eqtr4di ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
20 19 eqeq1d ⊢ ( 𝑗 = 𝐽 → ( ∪ 𝑗 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦 ) )
21 rexeq ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑛 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
22 19 21 raleqbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑛 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
23 20 22 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ∪ 𝑗 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑛 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ↔ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
24 23 abbidv ⊢ ( 𝑗 = 𝐽 → { 𝑦 ∣ ( ∪ 𝑗 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑛 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } = { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )
25 24 3 fvmptg ⊢ ( ( 𝐽 ∈ Top ∧ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ∈ V ) → ( LocFin ‘ 𝐽 ) = { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )
26 17 25 mpdan ⊢ ( 𝐽 ∈ Top → ( LocFin ‘ 𝐽 ) = { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } )
27 26 eleq2d ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ 𝐴 ∈ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ) )
28 elex ⊢ ( 𝐴 ∈ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } → 𝐴 ∈ V )
29 28 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ) → 𝐴 ∈ V )
30 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
31 30 2 eqtrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ) → 𝑋 = ∪ 𝐴 )
32 12 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ 𝐽 )
33 31 32 eqeltrrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 ∈ 𝐽 )
34 33 elexd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 ∈ V )
35 uniexb ⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
36 34 35 sylibr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ) → 𝐴 ∈ V )
37 36 adantrr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) → 𝐴 ∈ V )
38 unieq ⊢ ( 𝑦 = 𝐴 → ∪ 𝑦 = ∪ 𝐴 )
39 38 2 eqtr4di ⊢ ( 𝑦 = 𝐴 → ∪ 𝑦 = 𝑌 )
40 39 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = 𝑌 ) )
41 rabeq ⊢ ( 𝑦 = 𝐴 → { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } = { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } )
42 41 eleq1d ⊢ ( 𝑦 = 𝐴 → ( { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ↔ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
43 42 anbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
44 43 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
45 44 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
46 40 45 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
47 46 elabg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
48 29 37 47 pm5.21nd ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ { 𝑦 ∣ ( 𝑋 = ∪ 𝑦 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
49 27 48 bitrd ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
50 4 49 biadanii ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
51 3anass ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ↔ ( 𝐽 ∈ Top ∧ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) ) )
52 50 51 bitr4i ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )