Theorem locfinreflem

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 f from the original cover U , which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020)

	Ref	Expression
Hypotheses	locfinref.x	⊢ 𝑋 = ∪ 𝐽
	locfinref.1	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
	locfinref.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
	locfinref.3	⊢ ( 𝜑 → 𝑉 ⊆ 𝐽 )
	locfinref.4	⊢ ( 𝜑 → 𝑉 Ref 𝑈 )
	locfinref.5	⊢ ( 𝜑 → 𝑉 ∈ ( LocFin ‘ 𝐽 ) )
Assertion	locfinreflem	⊢ ( 𝜑 → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		locfinref.x	⊢ 𝑋 = ∪ 𝐽
2		locfinref.1	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
3		locfinref.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
4		locfinref.3	⊢ ( 𝜑 → 𝑉 ⊆ 𝐽 )
5		locfinref.4	⊢ ( 𝜑 → 𝑉 Ref 𝑈 )
6		locfinref.5	⊢ ( 𝜑 → 𝑉 ∈ ( LocFin ‘ 𝐽 ) )
7		reff	⊢ ( 𝑉 ∈ ( LocFin ‘ 𝐽 ) → ( 𝑉 Ref 𝑈 ↔ ( ∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃ 𝑔 ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝑉 Ref 𝑈 ↔ ( ∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃ 𝑔 ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) ) )
9	5 8	mpbid	⊢ ( 𝜑 → ( ∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃ 𝑔 ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) )
10	9	simprd	⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) )
11		funmpt	⊢ Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
12	11	a1i	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
13		eqid	⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
14	13	dmmptss	⊢ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ ran 𝑔
15		frn	⊢ ( 𝑔 : 𝑉 ⟶ 𝑈 → ran 𝑔 ⊆ 𝑈 )
16	15	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran 𝑔 ⊆ 𝑈 )
17	14 16	sstrid	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 )
18		locfintop	⊢ ( 𝑉 ∈ ( LocFin ‘ 𝐽 ) → 𝐽 ∈ Top )
19	6 18	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
20	19	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) → 𝐽 ∈ Top )
21		cnvimass	⊢ ( ◡ 𝑔 “ { 𝑢 } ) ⊆ dom 𝑔
22		fdm	⊢ ( 𝑔 : 𝑉 ⟶ 𝑈 → dom 𝑔 = 𝑉 )
23	22	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) → dom 𝑔 = 𝑉 )
24	21 23	sseqtrid	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) → ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝑉 )
25	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) → 𝑉 ⊆ 𝐽 )
26	24 25	sstrd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) → ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝐽 )
27		uniopn	⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝐽 ) → ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ 𝐽 )
28	20 26 27	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) → ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ 𝐽 )
29	28	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∀ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ 𝐽 )
30	13	rnmptss	⊢ ( ∀ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ 𝐽 → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 )
31	29 30	syl	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 )
32		eqid	⊢ ∪ 𝑉 = ∪ 𝑉
33		eqid	⊢ ∪ 𝑈 = ∪ 𝑈
34	32 33	refbas	⊢ ( 𝑉 Ref 𝑈 → ∪ 𝑈 = ∪ 𝑉 )
35	5 34	syl	⊢ ( 𝜑 → ∪ 𝑈 = ∪ 𝑉 )
36	35	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑈 = ∪ 𝑉 )
37		nfv	⊢ Ⅎ 𝑣 ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 )
38		nfra1	⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 )
39	37 38	nfan	⊢ Ⅎ 𝑣 ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
40		nfre1	⊢ Ⅎ 𝑣 ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣
41	39 40	nfan	⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
42		ffn	⊢ ( 𝑔 : 𝑉 ⟶ 𝑈 → 𝑔 Fn 𝑉 )
43	42	ad4antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑔 Fn 𝑉 )
44		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ 𝑉 )
45		fnfvelrn	⊢ ( ( 𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑔 ‘ 𝑣 ) ∈ ran 𝑔 )
46	43 44 45	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑔 ‘ 𝑣 ) ∈ ran 𝑔 )
47		ssid	⊢ 𝑣 ⊆ 𝑣
48	42	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑔 Fn 𝑉 )
49		eqid	⊢ ( 𝑔 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 )
50		fniniseg	⊢ ( 𝑔 Fn 𝑉 → ( 𝑣 ∈ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) )
51	50	biimpar	⊢ ( ( 𝑔 Fn 𝑉 ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) → 𝑣 ∈ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
52	49 51	mpanr2	⊢ ( ( 𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
53	48 52	sylancom	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
54		ssuni	⊢ ( ( 𝑣 ⊆ 𝑣 ∧ 𝑣 ∈ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) ) → 𝑣 ⊆ ∪ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
55	47 53 54	sylancr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ⊆ ∪ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
56	55	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ ∪ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
57		sneq	⊢ ( 𝑢 = ( 𝑔 ‘ 𝑣 ) → { 𝑢 } = { ( 𝑔 ‘ 𝑣 ) } )
58	57	imaeq2d	⊢ ( 𝑢 = ( 𝑔 ‘ 𝑣 ) → ( ◡ 𝑔 “ { 𝑢 } ) = ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
59	58	unieqd	⊢ ( 𝑢 = ( 𝑔 ‘ 𝑣 ) → ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) )
60	59	eleq2d	⊢ ( 𝑢 = ( 𝑔 ‘ 𝑣 ) → ( 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ↔ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) ) )
61	60	rspcev	⊢ ( ( ( 𝑔 ‘ 𝑣 ) ∈ ran 𝑔 ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { ( 𝑔 ‘ 𝑣 ) } ) ) → ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
62	46 56 61	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
63	62	adantllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
64		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ) → ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
65	41 63 64	r19.29af	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ) → ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
66		nfv	⊢ Ⅎ 𝑣 𝑢 ∈ ran 𝑔
67	39 66	nfan	⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 )
68		nfv	⊢ Ⅎ 𝑣 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } )
69	67 68	nfan	⊢ Ⅎ 𝑣 ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
70	24	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑥 ∈ 𝑣 ) → ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝑉 )
71		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) )
72	70 71	sseldd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ 𝑉 )
73		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ 𝑣 )
74		eluni2	⊢ ( 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ∃ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑥 ∈ 𝑣 )
75	74	bilani	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∃ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑥 ∈ 𝑣 )
76	69 72 73 75	reximd2a	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
77	76	r19.29an	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
78	65 77	impbida	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
79		eluni2	⊢ ( 𝑥 ∈ ∪ 𝑉 ↔ ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
80		eliun	⊢ ( 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
81	78 79 80	3bitr4g	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( 𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
82	81	eqrdv	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
83		dfiun3g	⊢ ( ∀ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ 𝐽 → ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
84	29 83	syl	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
85	36 82 84	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑈 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
86	15	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ran 𝑔 ⊆ 𝑈 )
87		vex	⊢ 𝑤 ∈ V
88	13	elrnmpt	⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ↔ ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
89	87 88	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ↔ ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
90	89	biimpa	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
91		ssrexv	⊢ ( ran 𝑔 ⊆ 𝑈 → ( ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) → ∃ 𝑢 ∈ 𝑈 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
92	86 90 91	sylc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ∃ 𝑢 ∈ 𝑈 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
93		nfv	⊢ Ⅎ 𝑢 ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
94		nfmpt1	⊢ Ⅎ 𝑢 ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
95	94	nfrn	⊢ Ⅎ 𝑢 ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
96	95	nfcri	⊢ Ⅎ 𝑢 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
97	93 96	nfan	⊢ Ⅎ 𝑢 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
98		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
99		nfv	⊢ Ⅎ 𝑣 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
100	39 99	nfan	⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
101		nfv	⊢ Ⅎ 𝑣 𝑢 ∈ 𝑈
102	100 101	nfan	⊢ Ⅎ 𝑣 ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 )
103		nfv	⊢ Ⅎ 𝑣 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } )
104	102 103	nfan	⊢ Ⅎ 𝑣 ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
105		simp-5r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
106	42	ad5antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑔 Fn 𝑉 )
107		fniniseg	⊢ ( 𝑔 Fn 𝑉 → ( 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = 𝑢 ) ) )
108	106 107	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = 𝑢 ) ) )
109	108	biimpa	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = 𝑢 ) )
110	109	simpld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑣 ∈ 𝑉 )
111		rspa	⊢ ( ( ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
112	105 110 111	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
113	109	simprd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑔 ‘ 𝑣 ) = 𝑢 )
114	112 113	sseqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑣 ⊆ 𝑢 )
115	114	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) → 𝑣 ⊆ 𝑢 ) )
116	104 115	ralrimi	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∀ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑣 ⊆ 𝑢 )
117		unissb	⊢ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝑢 ↔ ∀ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑣 ⊆ 𝑢 )
118	116 117	sylibr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∪ ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝑢 )
119	98 118	eqsstrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑤 ⊆ 𝑢 )
120	119	exp31	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ( 𝑢 ∈ 𝑈 → ( 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) → 𝑤 ⊆ 𝑢 ) ) )
121	97 120	reximdai	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) → ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 ) )
122	92 121	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 )
123	122	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∀ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 )
124		vex	⊢ 𝑔 ∈ V
125	124	rnex	⊢ ran 𝑔 ∈ V
126	125	mptex	⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V
127		rnexg	⊢ ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V )
128	126 127	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V )
129		eqid	⊢ ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
130	129 33	isref	⊢ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V → ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ↔ ( ∪ 𝑈 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ∀ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 ) ) )
131	128 130	syl	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ↔ ( ∪ 𝑈 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ∀ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 ) ) )
132	85 123 131	mpbir2and	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 )
133	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → 𝐽 ∈ Top )
134	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → 𝑋 = ∪ 𝑈 )
135	134 85	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → 𝑋 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
136		nfv	⊢ Ⅎ 𝑣 𝑥 ∈ 𝑋
137	39 136	nfan	⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 )
138		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) → 𝑣 ∈ 𝐽 )
139		ffun	⊢ ( 𝑔 : 𝑉 ⟶ 𝑈 → Fun 𝑔 )
140	139	ad6antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → Fun 𝑔 )
141		imafi	⊢ ( ( Fun 𝑔 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ∈ Fin )
142	140 141	sylancom	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ∈ Fin )
143		simp3	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) )
144		sneq	⊢ ( 𝑢 = 𝑘 → { 𝑢 } = { 𝑘 } )
145	144	imaeq2d	⊢ ( 𝑢 = 𝑘 → ( ◡ 𝑔 “ { 𝑢 } ) = ( ◡ 𝑔 “ { 𝑘 } ) )
146	145	unieqd	⊢ ( 𝑢 = 𝑘 → ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
147	124	cnvex	⊢ ◡ 𝑔 ∈ V
148		imaexg	⊢ ( ◡ 𝑔 ∈ V → ( ◡ 𝑔 “ { 𝑘 } ) ∈ V )
149	147 148	ax-mp	⊢ ( ◡ 𝑔 “ { 𝑘 } ) ∈ V
150	149	uniex	⊢ ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∈ V
151	146 13 150	fvmpt	⊢ ( 𝑘 ∈ ran 𝑔 → ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
152	151	3ad2ant2	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
153	143 152	eqtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
154	153	ineq1d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → ( 𝑤 ∩ 𝑣 ) = ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) )
155	154	neeq1d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → ( ( 𝑤 ∩ 𝑣 ) ≠ ∅ ↔ ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ ) )
156	125	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ran 𝑔 ∈ V )
157		imaexg	⊢ ( ◡ 𝑔 ∈ V → ( ◡ 𝑔 “ { 𝑢 } ) ∈ V )
158	147 157	ax-mp	⊢ ( ◡ 𝑔 “ { 𝑢 } ) ∈ V
159	158	uniex	⊢ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ V
160	159 13	fnmpti	⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Fn ran 𝑔
161		dffn4	⊢ ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Fn ran 𝑔 ↔ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) : ran 𝑔 –onto→ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
162	160 161	mpbi	⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) : ran 𝑔 –onto→ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
163	162	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) : ran 𝑔 –onto→ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
164	155 156 163	rabfodom	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑘 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ } )
165		sneq	⊢ ( 𝑘 = 𝑢 → { 𝑘 } = { 𝑢 } )
166	165	imaeq2d	⊢ ( 𝑘 = 𝑢 → ( ◡ 𝑔 “ { 𝑘 } ) = ( ◡ 𝑔 “ { 𝑢 } ) )
167	166	unieqd	⊢ ( 𝑘 = 𝑢 → ∪ ( ◡ 𝑔 “ { 𝑘 } ) = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
168	167	ineq1d	⊢ ( 𝑘 = 𝑢 → ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) = ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) )
169	168	neeq1d	⊢ ( 𝑘 = 𝑢 → ( ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ ↔ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) )
170	169	cbvrabv	⊢ { 𝑘 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ } = { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ }
171	164 170	breqtrdi	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } )
172	125	rabex	⊢ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ∈ V
173		nfv	⊢ Ⅎ 𝑗 ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 )
174		nfrab1	⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ }
175	174	nfel1	⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin
176	173 175	nfan	⊢ Ⅎ 𝑗 ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin )
177		nfv	⊢ Ⅎ 𝑗 𝑢 ∈ ran 𝑔
178	176 177	nfan	⊢ Ⅎ 𝑗 ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 )
179		nfv	⊢ Ⅎ 𝑗 ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅
180	178 179	nfan	⊢ Ⅎ 𝑗 ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ )
181		nfv	⊢ Ⅎ 𝑗 ( 𝑔 ‘ 𝑘 ) = 𝑢
182	174 181	nfrexw	⊢ Ⅎ 𝑗 ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢
183	42	ad5antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑔 Fn 𝑉 )
184	183	ad5antr	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑔 Fn 𝑉 )
185		simplr	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) )
186		fniniseg	⊢ ( 𝑔 Fn 𝑉 → ( 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ( 𝑗 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) ) )
187	186	biimpa	⊢ ( ( 𝑔 Fn 𝑉 ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑗 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) )
188	184 185 187	syl2anc	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ( 𝑗 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) )
189	188	simpld	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑗 ∈ 𝑉 )
190		simpr	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
191		rabid	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ↔ ( 𝑗 ∈ 𝑉 ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) )
192	189 190 191	sylanbrc	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑗 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } )
193	188	simprd	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ( 𝑔 ‘ 𝑗 ) = 𝑢 )
194		fveqeq2	⊢ ( 𝑘 = 𝑗 → ( ( 𝑔 ‘ 𝑘 ) = 𝑢 ↔ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) )
195	194	rspcev	⊢ ( ( 𝑗 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 )
196	192 193 195	syl2anc	⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 )
197		uniinn0	⊢ ( ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ↔ ∃ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
198	197	bilani	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) → ∃ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
199	180 182 196 198	r19.29af2	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 )
200	199	ex	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) → ( ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 ) )
201	200	ss2rabdv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ⊆ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
202		ssdomg	⊢ ( { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ∈ V → ( { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ⊆ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } → { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ) )
203	172 201 202	mpsyl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
204		domtr	⊢ ( ( { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ∧ { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
205	171 203 204	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
206	183	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → 𝑔 Fn 𝑉 )
207		dffn3	⊢ ( 𝑔 Fn 𝑉 ↔ 𝑔 : 𝑉 ⟶ ran 𝑔 )
208	207	biimpi	⊢ ( 𝑔 Fn 𝑉 → 𝑔 : 𝑉 ⟶ ran 𝑔 )
209		ssrab2	⊢ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ⊆ 𝑉
210		fimarab	⊢ ( ( 𝑔 : 𝑉 ⟶ ran 𝑔 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ⊆ 𝑉 ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) = { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
211	209 210	mpan2	⊢ ( 𝑔 : 𝑉 ⟶ ran 𝑔 → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) = { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
212	206 208 211	3syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) = { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
213	205 212	breqtrrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) )
214		domfi	⊢ ( ( ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ∈ Fin ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin )
215	142 213 214	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin )
216	215	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ( { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
217	216	imdistanda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
218	217	imp	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) → ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
219		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
220	1 32	islocfin	⊢ ( 𝑉 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
221	6 220	sylib	⊢ ( 𝜑 → ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
222	221	simp3d	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
223	222	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
224	219 223	sylancom	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
225	137 138 218 224	reximd2a	⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
226	225	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
227	1 129	islocfin	⊢ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
228	133 135 226 227	syl3anbrc	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) )
229		funeq	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( Fun 𝑓 ↔ Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) )
230		dmeq	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → dom 𝑓 = dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
231	230	sseq1d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( dom 𝑓 ⊆ 𝑈 ↔ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ) )
232		rneq	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ran 𝑓 = ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
233	232	sseq1d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ran 𝑓 ⊆ 𝐽 ↔ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) )
234	229 231 233	3anbi123d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ↔ ( Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) ) )
235	232	breq1d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ran 𝑓 Ref 𝑈 ↔ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ) )
236	232	eleq1d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ↔ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) )
237	235 236	anbi12d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ↔ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) )
238	234 237	anbi12d	⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) ↔ ( ( Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) ∧ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) ) )
239	126 238	spcev	⊢ ( ( ( Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) ∧ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )
240	12 17 31 132 228 239	syl32anc	⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )
241	240	expl	⊢ ( 𝜑 → ( ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) ) )
242	241	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) ) )
243	10 242	mpd	⊢ ( 𝜑 → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )