Theorem locfinref 30718

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.

Step	Hyp	Ref	Expression
1		f0 6435	. . . 4 ⊢ ∅:∅⟶𝐽
2		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = ∅) → 𝑈 = ∅)
3	2	feq2d 6375	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = ∅) → (∅:𝑈⟶𝐽 ↔ ∅:∅⟶𝐽))
4	1, 3	mpbiri 259	. . 3 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ∅:𝑈⟶𝐽)
5		rn0 5722	. . . . 5 ⊢ ran ∅ = ∅
6		0ex 5109	. . . . . 6 ⊢ ∅ ∈ V
7		refref 21809	. . . . . 6 ⊢ (∅ ∈ V → ∅Ref∅)
8	6, 7	ax-mp 5	. . . . 5 ⊢ ∅Ref∅
9	5, 8	eqbrtri 4989	. . . 4 ⊢ ran ∅Ref∅
10	9, 2	breqtrrid 5006	. . 3 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ran ∅Ref𝑈)
11		sn0top 21295	. . . . . 6 ⊢ {∅} ∈ Top
12	11	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = ∅) → {∅} ∈ Top)
13		eqidd 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ∅ = ∅)
14		ral0 4376	. . . . . 6 ⊢ ∀𝑥 ∈ ∅ ∃𝑛 ∈ {∅} (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ ran ∅ ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)
15	14	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ∀𝑥 ∈ ∅ ∃𝑛 ∈ {∅} (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ ran ∅ ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))
16	6	unisn 4767	. . . . . . 7 ⊢ ∪ {∅} = ∅
17	16	eqcomi 2806	. . . . . 6 ⊢ ∅ = ∪ {∅}
18	5	unieqi 4760	. . . . . . 7 ⊢ ∪ ran ∅ = ∪ ∅
19		uni0 4778	. . . . . . 7 ⊢ ∪ ∅ = ∅
20	18, 19	eqtr2i 2822	. . . . . 6 ⊢ ∅ = ∪ ran ∅
21	17, 20	islocfin 21813	. . . . 5 ⊢ (ran ∅ ∈ (LocFin‘{∅}) ↔ ({∅} ∈ Top ∧ ∅ = ∅ ∧ ∀𝑥 ∈ ∅ ∃𝑛 ∈ {∅} (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ ran ∅ ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)))
22	12, 13, 15, 21	syl3anbrc 1336	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ran ∅ ∈ (LocFin‘{∅}))
23		locfinref.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 = ∪ 𝑈)
24	23	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 = ∅) → 𝑋 = ∪ 𝑈)
25	2	unieqd 4761	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ∪ 𝑈 = ∪ ∅)
26	24, 25	eqtrd 2833	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 = ∅) → 𝑋 = ∪ ∅)
27		locfinref.x	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
28	26, 27, 19	3eqtr3g 2856	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ∪ 𝐽 = ∅)
29		locfinref.5	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽))
30		locfintop 21817	. . . . . . . 8 ⊢ (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
31		0top 21279	. . . . . . . 8 ⊢ (𝐽 ∈ Top → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅}))
32	29, 30, 31	3syl 18	. . . . . . 7 ⊢ (𝜑 → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅}))
33	32	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = ∅) → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅}))
34	28, 33	mpbid 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = ∅) → 𝐽 = {∅})
35	34	fveq2d 6549	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = ∅) → (LocFin‘𝐽) = (LocFin‘{∅}))
36	22, 35	eleqtrrd 2888	. . 3 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ran ∅ ∈ (LocFin‘𝐽))
37		feq1 6370	. . . . 5 ⊢ (𝑓 = ∅ → (𝑓:𝑈⟶𝐽 ↔ ∅:𝑈⟶𝐽))
38		rneq 5695	. . . . . 6 ⊢ (𝑓 = ∅ → ran 𝑓 = ran ∅)
39	38	breq1d 4978	. . . . 5 ⊢ (𝑓 = ∅ → (ran 𝑓Ref𝑈 ↔ ran ∅Ref𝑈))
40	38	eleq1d 2869	. . . . 5 ⊢ (𝑓 = ∅ → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran ∅ ∈ (LocFin‘𝐽)))
41	37, 39, 40	3anbi123d 1428	. . . 4 ⊢ (𝑓 = ∅ → ((𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (∅:𝑈⟶𝐽 ∧ ran ∅Ref𝑈 ∧ ran ∅ ∈ (LocFin‘𝐽))))
42	6, 41	spcev 3551	. . 3 ⊢ ((∅:𝑈⟶𝐽 ∧ ran ∅Ref𝑈 ∧ ran ∅ ∈ (LocFin‘𝐽)) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
43	4, 10, 36, 42	syl3anc 1364	. 2 ⊢ ((𝜑 ∧ 𝑈 = ∅) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
44		locfinref.1	. . . . 5 ⊢ (𝜑 → 𝑈 ⊆ 𝐽)
45		locfinref.3	. . . . 5 ⊢ (𝜑 → 𝑉 ⊆ 𝐽)
46		locfinref.4	. . . . 5 ⊢ (𝜑 → 𝑉Ref𝑈)
47	27, 44, 23, 45, 46, 29	locfinreflem 30717	. . . 4 ⊢ (𝜑 → ∃𝑔((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽))))
48	47	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ ∅) → ∃𝑔((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽))))
49		simpl 483	. . . 4 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (𝜑 ∧ 𝑈 ≠ ∅))
50		simprl1 1211	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → Fun 𝑔)
51		fdmrn 6413	. . . . . . . 8 ⊢ (Fun 𝑔 ↔ 𝑔:dom 𝑔⟶ran 𝑔)
52	50, 51	sylib 219	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → 𝑔:dom 𝑔⟶ran 𝑔)
53		simprl3 1213	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran 𝑔 ⊆ 𝐽)
54	52, 53	fssd 6403	. . . . . 6 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → 𝑔:dom 𝑔⟶𝐽)
55		fconstg 6441	. . . . . . . 8 ⊢ (∅ ∈ V → ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶{∅})
56	6, 55	mp1i 13	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶{∅})
57		0opn 21200	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)
58	29, 30, 57	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ 𝐽)
59	58	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ∅ ∈ 𝐽)
60	59	snssd 4655	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → {∅} ⊆ 𝐽)
61	56, 60	fssd 6403	. . . . . 6 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶𝐽)
62		disjdif 4341	. . . . . . 7 ⊢ (dom 𝑔 ∩ (𝑈 ∖ dom 𝑔)) = ∅
63	62	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (dom 𝑔 ∩ (𝑈 ∖ dom 𝑔)) = ∅)
64		fun2 6416	. . . . . 6 ⊢ (((𝑔:dom 𝑔⟶𝐽 ∧ ((𝑈 ∖ dom 𝑔) × {∅}):(𝑈 ∖ dom 𝑔)⟶𝐽) ∧ (dom 𝑔 ∩ (𝑈 ∖ dom 𝑔)) = ∅) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):(dom 𝑔 ∪ (𝑈 ∖ dom 𝑔))⟶𝐽)
65	54, 61, 63, 64	syl21anc 834	. . . . 5 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):(dom 𝑔 ∪ (𝑈 ∖ dom 𝑔))⟶𝐽)
66		simprl2 1212	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → dom 𝑔 ⊆ 𝑈)
67		undif 4350	. . . . . . 7 ⊢ (dom 𝑔 ⊆ 𝑈 ↔ (dom 𝑔 ∪ (𝑈 ∖ dom 𝑔)) = 𝑈)
68	66, 67	sylib 219	. . . . . 6 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (dom 𝑔 ∪ (𝑈 ∖ dom 𝑔)) = 𝑈)
69	68	feq2d 6375	. . . . 5 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):(dom 𝑔 ∪ (𝑈 ∖ dom 𝑔))⟶𝐽 ↔ (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽))
70	65, 69	mpbid 233	. . . 4 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽)
71		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔)
72		simprrl 777	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran 𝑔Ref𝑈)
73	72	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran 𝑔Ref𝑈)
74	71, 73	eqbrtrd 4990	. . . . 5 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈)
75		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅}))
76	49	simprd 496	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → 𝑈 ≠ ∅)
77		refun0 21811	. . . . . . . 8 ⊢ ((ran 𝑔Ref𝑈 ∧ 𝑈 ≠ ∅) → (ran 𝑔 ∪ {∅})Ref𝑈)
78	72, 76, 77	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (ran 𝑔 ∪ {∅})Ref𝑈)
79	78	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → (ran 𝑔 ∪ {∅})Ref𝑈)
80	75, 79	eqbrtrd 4990	. . . . 5 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈)
81		rnxpss 5912	. . . . . . 7 ⊢ ran ((𝑈 ∖ dom 𝑔) × {∅}) ⊆ {∅}
82		sssn 4672	. . . . . . 7 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) ⊆ {∅} ↔ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ ∨ ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅}))
83	81, 82	mpbi 231	. . . . . 6 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ ∨ ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅})
84		rnun 5887	. . . . . . . . 9 ⊢ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ ran ((𝑈 ∖ dom 𝑔) × {∅}))
85		uneq2 4060	. . . . . . . . 9 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ → (ran 𝑔 ∪ ran ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ ∅))
86	84, 85	syl5eq 2845	. . . . . . . 8 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ ∅))
87		un0 4270	. . . . . . . 8 ⊢ (ran 𝑔 ∪ ∅) = ran 𝑔
88	86, 87	syl6eq 2849	. . . . . . 7 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔)
89		uneq2 4060	. . . . . . . 8 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅} → (ran 𝑔 ∪ ran ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅}))
90	84, 89	syl5eq 2845	. . . . . . 7 ⊢ (ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅} → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅}))
91	88, 90	orim12i 903	. . . . . 6 ⊢ ((ran ((𝑈 ∖ dom 𝑔) × {∅}) = ∅ ∨ ran ((𝑈 ∖ dom 𝑔) × {∅}) = {∅}) → (ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔 ∨ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})))
92	83, 91	mp1i 13	. . . . 5 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → (ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔 ∨ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})))
93	74, 80, 92	mpjaodan 953	. . . 4 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈)
94		simprrr 778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran 𝑔 ∈ (LocFin‘𝐽))
95	94	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran 𝑔 ∈ (LocFin‘𝐽))
96	71, 95	eqeltrd 2885	. . . . 5 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = ran 𝑔) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))
97	94	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran 𝑔 ∈ (LocFin‘𝐽))
98		snfi 8449	. . . . . . . 8 ⊢ {∅} ∈ Fin
99	98	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → {∅} ∈ Fin)
100	59	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ∅ ∈ 𝐽)
101	100	snssd 4655	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → {∅} ⊆ 𝐽)
102	101	unissd 4775	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ∪ {∅} ⊆ ∪ 𝐽)
103		lfinun 21821	. . . . . . 7 ⊢ ((ran 𝑔 ∈ (LocFin‘𝐽) ∧ {∅} ∈ Fin ∧ ∪ {∅} ⊆ ∪ 𝐽) → (ran 𝑔 ∪ {∅}) ∈ (LocFin‘𝐽))
104	97, 99, 102, 103	syl3anc 1364	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → (ran 𝑔 ∪ {∅}) ∈ (LocFin‘𝐽))
105	75, 104	eqeltrd 2885	. . . . 5 ⊢ ((((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) = (ran 𝑔 ∪ {∅})) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))
106	96, 105, 92	mpjaodan 953	. . . 4 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))
107		refrel 21804	. . . . . . . . 9 ⊢ Rel Ref
108	107	brrelex2i 5502	. . . . . . . 8 ⊢ (𝑉Ref𝑈 → 𝑈 ∈ V)
109		difexg 5129	. . . . . . . 8 ⊢ (𝑈 ∈ V → (𝑈 ∖ dom 𝑔) ∈ V)
110	46, 108, 109	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∖ dom 𝑔) ∈ V)
111	110	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 ≠ ∅) → (𝑈 ∖ dom 𝑔) ∈ V)
112		p0ex 5182	. . . . . . 7 ⊢ {∅} ∈ V
113		xpexg 7337	. . . . . . 7 ⊢ (((𝑈 ∖ dom 𝑔) ∈ V ∧ {∅} ∈ V) → ((𝑈 ∖ dom 𝑔) × {∅}) ∈ V)
114	112, 113	mpan2 687	. . . . . 6 ⊢ ((𝑈 ∖ dom 𝑔) ∈ V → ((𝑈 ∖ dom 𝑔) × {∅}) ∈ V)
115		vex 3443	. . . . . . 7 ⊢ 𝑔 ∈ V
116		unexg 7336	. . . . . . 7 ⊢ ((𝑔 ∈ V ∧ ((𝑈 ∖ dom 𝑔) × {∅}) ∈ V) → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ V)
117	115, 116	mpan 686	. . . . . 6 ⊢ (((𝑈 ∖ dom 𝑔) × {∅}) ∈ V → (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ V)
118		feq1 6370	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → (𝑓:𝑈⟶𝐽 ↔ (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽))
119		rneq 5695	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → ran 𝑓 = ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})))
120	119	breq1d 4978	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → (ran 𝑓Ref𝑈 ↔ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈))
121	119	eleq1d 2869	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽)))
122	118, 120, 121	3anbi123d 1428	. . . . . . 7 ⊢ (𝑓 = (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) → ((𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))))
123	122	spcegv 3542	. . . . . 6 ⊢ ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ V → (((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽)) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
124	111, 114, 117, 123	4syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 ≠ ∅) → (((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽)) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
125	124	imp 407	. . . 4 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})):𝑈⟶𝐽 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅}))Ref𝑈 ∧ ran (𝑔 ∪ ((𝑈 ∖ dom 𝑔) × {∅})) ∈ (LocFin‘𝐽))) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
126	49, 70, 93, 106, 125	syl13anc 1365	. . 3 ⊢ (((𝜑 ∧ 𝑈 ≠ ∅) ∧ ((Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽) ∧ (ran 𝑔Ref𝑈 ∧ ran 𝑔 ∈ (LocFin‘𝐽)))) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
127	48, 126	exlimddv 1917	. 2 ⊢ ((𝜑 ∧ 𝑈 ≠ ∅) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
128	43, 127	pm2.61dane 3074	1 ⊢ (𝜑 → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1525  ∃wex 1765   ∈ wcel 2083   ≠ wne 2986  ∀wral 3107  ∃wrex 3108  {crab 3111  Vcvv 3440   ∖ cdif 3862   ∪ cun 3863   ∩ cin 3864   ⊆ wss 3865  ∅c0 4217  {csn 4478  ∪ cuni 4751   class class class wbr 4968   × cxp 5448  dom cdm 5450  ran crn 5451  Fun wfun 6226  ⟶wf 6228  ‘cfv 6232  Fincfn 8364  Topctop 21189  Refcref 21798  LocFinclocfin 21800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-reg 8909  ax-inf2 8957  ax-ac2 9738

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-en 8365  df-dom 8366  df-fin 8368  df-r1 9046  df-rank 9047  df-card 9221  df-ac 9395  df-top 21190  df-topon 21207  df-ref 21801  df-locfin 21803

This theorem is referenced by:  pcmplfinf  30738