Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  locfinref Structured version   Visualization version   GIF version

Theorem locfinref 29236
Description: A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.)
Hypotheses
Ref Expression
locfinref.x 𝑋 = 𝐽
locfinref.1 (𝜑𝑈𝐽)
locfinref.2 (𝜑𝑋 = 𝑈)
locfinref.3 (𝜑𝑉𝐽)
locfinref.4 (𝜑𝑉Ref𝑈)
locfinref.5 (𝜑𝑉 ∈ (LocFin‘𝐽))
Assertion
Ref Expression
locfinref (𝜑 → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
Distinct variable groups:   𝑓,𝐽   𝑈,𝑓   𝑓,𝑉   𝜑,𝑓
Allowed substitution hint:   𝑋(𝑓)

Proof of Theorem locfinref
Dummy variables 𝑔 𝑥 𝑛 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f0 5999 . . . 4 ∅:∅⟶𝐽
2 simpr 476 . . . . 5 ((𝜑𝑈 = ∅) → 𝑈 = ∅)
32feq2d 5944 . . . 4 ((𝜑𝑈 = ∅) → (∅:𝑈𝐽 ↔ ∅:∅⟶𝐽))
41, 3mpbiri 247 . . 3 ((𝜑𝑈 = ∅) → ∅:𝑈𝐽)
5 rn0 5298 . . . . 5 ran ∅ = ∅
6 0ex 4718 . . . . . 6 ∅ ∈ V
7 refref 21126 . . . . . 6 (∅ ∈ V → ∅Ref∅)
86, 7ax-mp 5 . . . . 5 ∅Ref∅
95, 8eqbrtri 4604 . . . 4 ran ∅Ref∅
109, 2syl5breqr 4621 . . 3 ((𝜑𝑈 = ∅) → ran ∅Ref𝑈)
11 sn0top 20613 . . . . . 6 {∅} ∈ Top
1211a1i 11 . . . . 5 ((𝜑𝑈 = ∅) → {∅} ∈ Top)
13 eqidd 2611 . . . . 5 ((𝜑𝑈 = ∅) → ∅ = ∅)
14 ral0 4028 . . . . . 6 𝑥 ∈ ∅ ∃𝑛 ∈ {∅} (𝑥𝑛 ∧ {𝑠 ∈ ran ∅ ∣ (𝑠𝑛) ≠ ∅} ∈ Fin)
1514a1i 11 . . . . 5 ((𝜑𝑈 = ∅) → ∀𝑥 ∈ ∅ ∃𝑛 ∈ {∅} (𝑥𝑛 ∧ {𝑠 ∈ ran ∅ ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))
166unisn 4387 . . . . . . 7 {∅} = ∅
1716eqcomi 2619 . . . . . 6 ∅ = {∅}
185unieqi 4381 . . . . . . 7 ran ∅ =
19 uni0 4401 . . . . . . 7 ∅ = ∅
2018, 19eqtr2i 2633 . . . . . 6 ∅ = ran ∅
2117, 20islocfin 21130 . . . . 5 (ran ∅ ∈ (LocFin‘{∅}) ↔ ({∅} ∈ Top ∧ ∅ = ∅ ∧ ∀𝑥 ∈ ∅ ∃𝑛 ∈ {∅} (𝑥𝑛 ∧ {𝑠 ∈ ran ∅ ∣ (𝑠𝑛) ≠ ∅} ∈ Fin)))
2212, 13, 15, 21syl3anbrc 1239 . . . 4 ((𝜑𝑈 = ∅) → ran ∅ ∈ (LocFin‘{∅}))
23 locfinref.2 . . . . . . . . 9 (𝜑𝑋 = 𝑈)
2423adantr 480 . . . . . . . 8 ((𝜑𝑈 = ∅) → 𝑋 = 𝑈)
252unieqd 4382 . . . . . . . 8 ((𝜑𝑈 = ∅) → 𝑈 = ∅)
2624, 25eqtrd 2644 . . . . . . 7 ((𝜑𝑈 = ∅) → 𝑋 = ∅)
27 locfinref.x . . . . . . 7 𝑋 = 𝐽
2826, 27, 193eqtr3g 2667 . . . . . 6 ((𝜑𝑈 = ∅) → 𝐽 = ∅)
29 locfinref.5 . . . . . . . 8 (𝜑𝑉 ∈ (LocFin‘𝐽))
30 locfintop 21134 . . . . . . . 8 (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
31 0top 20598 . . . . . . . 8 (𝐽 ∈ Top → ( 𝐽 = ∅ ↔ 𝐽 = {∅}))
3229, 30, 313syl 18 . . . . . . 7 (𝜑 → ( 𝐽 = ∅ ↔ 𝐽 = {∅}))
3332adantr 480 . . . . . 6 ((𝜑𝑈 = ∅) → ( 𝐽 = ∅ ↔ 𝐽 = {∅}))
3428, 33mpbid 221 . . . . 5 ((𝜑𝑈 = ∅) → 𝐽 = {∅})
3534fveq2d 6107 . . . 4 ((𝜑𝑈 = ∅) → (LocFin‘𝐽) = (LocFin‘{∅}))
3622, 35eleqtrrd 2691 . . 3 ((𝜑𝑈 = ∅) → ran ∅ ∈ (LocFin‘𝐽))
37 feq1 5939 . . . . 5 (𝑓 = ∅ → (𝑓:𝑈𝐽 ↔ ∅:𝑈𝐽))
38 rneq 5272 . . . . . 6 (𝑓 = ∅ → ran 𝑓 = ran ∅)
3938breq1d 4593 . . . . 5 (𝑓 = ∅ → (ran 𝑓Ref𝑈 ↔ ran ∅Ref𝑈))
4038eleq1d 2672 . . . . 5 (𝑓 = ∅ → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran ∅ ∈ (LocFin‘𝐽)))
4137, 39, 403anbi123d 1391 . . . 4 (𝑓 = ∅ → ((𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (∅:𝑈𝐽 ∧ ran ∅Ref𝑈 ∧ ran ∅ ∈ (LocFin‘𝐽))))
426, 41spcev 3273 . . 3 ((∅:𝑈𝐽 ∧ ran ∅Ref𝑈 ∧ ran ∅ ∈ (LocFin‘𝐽)) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
434, 10, 36, 42syl3anc 1318 . 2 ((𝜑𝑈 = ∅) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
44 locfinref.1 . . . . 5 (𝜑𝑈𝐽)
45 locfinref.3 . . . . 5 (𝜑𝑉𝐽)
46 locfinref.4 . . . . 5 (𝜑𝑉Ref𝑈)
4727, 44, 23, 45, 46, 29locfinreflem 29235 . . . 4 (𝜑 → ∃𝑔((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽))))
4847adantr 480 . . 3 ((𝜑𝑈 ≠ ∅) → ∃𝑔((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽))))
49 simpl 472 . . . 4 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (𝜑𝑈 ≠ ∅))
50 simprl1 1099 . . . . . . . 8 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → Fun 𝑔)
51 fdmrn 5977 . . . . . . . 8 (Fun 𝑔𝑔:dom 𝑔⟶ran 𝑔)
5250, 51sylib 207 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → 𝑔:dom 𝑔⟶ran 𝑔)
53 simprl3 1101 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran 𝑔𝐽)
5452, 53fssd 5970 . . . . . 6 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → 𝑔:dom 𝑔𝐽)
55 fconstg 6005 . . . . . . . 8 (∅ ∈ V → ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶{∅})
566, 55mp1i 13 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶{∅})
57 0opn 20534 . . . . . . . . . 10 (𝐽 ∈ Top → ∅ ∈ 𝐽)
5829, 30, 573syl 18 . . . . . . . . 9 (𝜑 → ∅ ∈ 𝐽)
5958ad2antrr 758 . . . . . . . 8 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ∅ ∈ 𝐽)
6059snssd 4281 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → {∅} ⊆ 𝐽)
6156, 60fssd 5970 . . . . . 6 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶𝐽)
62 disjdif 3992 . . . . . . 7 (dom 𝑔 ∩ (𝑈 ∖ dom 𝑔)) = ∅
6362a1i 11 . . . . . 6 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (dom 𝑔 ∩ (𝑈 ∖ dom 𝑔)) = ∅)
64 fun2 5980 . . . . . 6 (((𝑔:dom 𝑔𝐽 ∧ ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶𝐽) ∧ (dom 𝑔 ∩ (𝑈 ∖ dom 𝑔)) = ∅) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):(dom 𝑔 ∪ (𝑈 ∖ dom 𝑔))⟶𝐽)
6554, 61, 63, 64syl21anc 1317 . . . . 5 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):(dom 𝑔 ∪ (𝑈 ∖ dom 𝑔))⟶𝐽)
66 simprl2 1100 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → dom 𝑔𝑈)
67 undif 4001 . . . . . . 7 (dom 𝑔𝑈 ↔ (dom 𝑔 ∪ (𝑈 ∖ dom 𝑔)) = 𝑈)
6866, 67sylib 207 . . . . . 6 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (dom 𝑔 ∪ (𝑈 ∖ dom 𝑔)) = 𝑈)
6968feq2d 5944 . . . . 5 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):(dom 𝑔 ∪ (𝑈 ∖ dom 𝑔))⟶𝐽 ↔ (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽))
7065, 69mpbid 221 . . . 4 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽)
71 simpr 476 . . . . . 6 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔)
72 simprrl 800 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran 𝑔Ref𝑈)
7372adantr 480 . . . . . 6 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran 𝑔Ref𝑈)
7471, 73eqbrtrd 4605 . . . . 5 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈)
75 simpr 476 . . . . . 6 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅}))
7649simprd 478 . . . . . . . 8 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → 𝑈 ≠ ∅)
77 refun0 21128 . . . . . . . 8 ((ran 𝑔Ref𝑈𝑈 ≠ ∅) → (ran 𝑔 ∪ {∅})Ref𝑈)
7872, 76, 77syl2anc 691 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (ran 𝑔 ∪ {∅})Ref𝑈)
7978adantr 480 . . . . . 6 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → (ran 𝑔 ∪ {∅})Ref𝑈)
8075, 79eqbrtrd 4605 . . . . 5 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈)
81 rnxpss 5485 . . . . . . 7 ran ((𝑈 ∖ dom 𝑔) × {∅}) ⊆ {∅}
82 sssn 4298 . . . . . . 7 (ran ((𝑈 ∖ dom 𝑔) × {∅}) ⊆ {∅} ↔ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ ∨ ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅}))
8381, 82mpbi 219 . . . . . 6 (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ ∨ ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅})
84 rnun 5460 . . . . . . . . 9 ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ ran ((𝑈 ∖ dom 𝑔) × {∅}))
85 uneq2 3723 . . . . . . . . 9 (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ → (ran 𝑔 ∪ ran ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ ∅))
8684, 85syl5eq 2656 . . . . . . . 8 (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ ∅))
87 un0 3919 . . . . . . . 8 (ran 𝑔 ∪ ∅) = ran 𝑔
8886, 87syl6eq 2660 . . . . . . 7 (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔)
89 uneq2 3723 . . . . . . . 8 (ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅} → (ran 𝑔 ∪ ran ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅}))
9084, 89syl5eq 2656 . . . . . . 7 (ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅} → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅}))
9188, 90orim12i 537 . . . . . 6 ((ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ ∨ ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅}) → (ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔 ∨ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})))
9283, 91mp1i 13 . . . . 5 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔 ∨ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})))
9374, 80, 92mpjaodan 823 . . . 4 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈)
94 simprrr 801 . . . . . . 7 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran 𝑔 ∈ (LocFin‘𝐽))
9594adantr 480 . . . . . 6 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran 𝑔 ∈ (LocFin‘𝐽))
9671, 95eqeltrd 2688 . . . . 5 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))
9794adantr 480 . . . . . . 7 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran 𝑔 ∈ (LocFin‘𝐽))
98 snfi 7923 . . . . . . . 8 {∅} ∈ Fin
9998a1i 11 . . . . . . 7 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → {∅} ∈ Fin)
10059adantr 480 . . . . . . . . 9 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ∅ ∈ 𝐽)
101100snssd 4281 . . . . . . . 8 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → {∅} ⊆ 𝐽)
102101unissd 4398 . . . . . . 7 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → {∅} ⊆ 𝐽)
103 lfinun 21138 . . . . . . 7 ((ran 𝑔 ∈ (LocFin‘𝐽) ∧ {∅} ∈ Fin ∧ {∅} ⊆ 𝐽) → (ran 𝑔 ∪ {∅}) ∈ (LocFin‘𝐽))
10497, 99, 102, 103syl3anc 1318 . . . . . 6 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → (ran 𝑔 ∪ {∅}) ∈ (LocFin‘𝐽))
10575, 104eqeltrd 2688 . . . . 5 ((((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))
10696, 105, 92mpjaodan 823 . . . 4 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))
107 refrel 21121 . . . . . . . . 9 Rel Ref
108107brrelex2i 5083 . . . . . . . 8 (𝑉Ref𝑈𝑈 ∈ V)
109 difexg 4735 . . . . . . . 8 (𝑈 ∈ V → (𝑈 ∖ dom 𝑔) ∈ V)
11046, 108, 1093syl 18 . . . . . . 7 (𝜑 → (𝑈 ∖ dom 𝑔) ∈ V)
111110adantr 480 . . . . . 6 ((𝜑𝑈 ≠ ∅) → (𝑈 ∖ dom 𝑔) ∈ V)
112 p0ex 4779 . . . . . . 7 {∅} ∈ V
113 xpexg 6858 . . . . . . 7 (((𝑈 ∖ dom 𝑔) ∈ V ∧ {∅} ∈ V) → ((𝑈 ∖ dom 𝑔) × {∅}) ∈ V)
114112, 113mpan2 703 . . . . . 6 ((𝑈 ∖ dom 𝑔) ∈ V → ((𝑈 ∖ dom 𝑔) × {∅}) ∈ V)
115 vex 3176 . . . . . . 7 𝑔 ∈ V
116 unexg 6857 . . . . . . 7 ((𝑔 ∈ V ∧ ((𝑈 ∖ dom 𝑔) × {∅}) ∈ V) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ V)
117115, 116mpan 702 . . . . . 6 (((𝑈 ∖ dom 𝑔) × {∅}) ∈ V → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ V)
118 feq1 5939 . . . . . . . 8 (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → (𝑓:𝑈𝐽 ↔ (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽))
119 rneq 5272 . . . . . . . . 9 (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → ran 𝑓 = ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})))
120119breq1d 4593 . . . . . . . 8 (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → (ran 𝑓Ref𝑈 ↔ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈))
121119eleq1d 2672 . . . . . . . 8 (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽)))
122118, 120, 1213anbi123d 1391 . . . . . . 7 (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → ((𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))))
123122spcegv 3267 . . . . . 6 ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ V → (((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽)) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
124111, 114, 117, 1234syl 19 . . . . 5 ((𝜑𝑈 ≠ ∅) → (((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽)) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
125124imp 444 . . . 4 (((𝜑𝑈 ≠ ∅) ∧ ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
12649, 70, 93, 106, 125syl13anc 1320 . . 3 (((𝜑𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔𝑈 ∧ ran 𝑔𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
12748, 126exlimddv 1850 . 2 ((𝜑𝑈 ≠ ∅) → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
12843, 127pm2.61dane 2869 1 (𝜑 → ∃𝑓(𝑓:𝑈𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wo 382  wa 383  w3a 1031   = wceq 1475  wex 1695  wcel 1977  wne 2780  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  {csn 4125   cuni 4372   class class class wbr 4583   × cxp 5036  dom cdm 5038  ran crn 5039  Fun wfun 5798  wf 5800  cfv 5804  Fincfn 7841  Topctop 20517  Refcref 21115  LocFinclocfin 21117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-reg 8380  ax-inf2 8421  ax-ac2 9168
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-fin 7845  df-r1 8510  df-rank 8511  df-card 8648  df-ac 8822  df-top 20521  df-topon 20523  df-ref 21118  df-locfin 21120
This theorem is referenced by:  pcmplfinf  29256
  Copyright terms: Public domain W3C validator