Metamath Proof Explorer

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 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
75 eluni2 ⊢ ( 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ∃ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑥 ∈ 𝑣 )
76 74 75 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∃ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑥 ∈ 𝑣 )
77 69 72 73 76 reximd2a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
78 77 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
79 65 78 impbida ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
80 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑉 ↔ ∃ 𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 )
81 eliun ⊢ ( 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ∃ 𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
82 79 80 81 3bitr4g ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( 𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
83 82 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
84 dfiun3g ⊢ ( ∀ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ 𝐽 → ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
85 29 84 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑢 ∈ ran 𝑔 ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
86 36 83 85 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∪ 𝑈 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
87 15 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ran 𝑔 ⊆ 𝑈 )
88 vex ⊢ 𝑤 ∈ V
89 13 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ↔ ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
90 88 89 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ↔ ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
91 90 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
92 ssrexv ⊢ ( ran 𝑔 ⊆ 𝑈 → ( ∃ 𝑢 ∈ ran 𝑔 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) → ∃ 𝑢 ∈ 𝑈 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
93 87 91 92 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ∃ 𝑢 ∈ 𝑈 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
94 nfv ⊢ Ⅎ 𝑢 ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
95 nfmpt1 ⊢ Ⅎ 𝑢 ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
96 95 nfrn ⊢ Ⅎ 𝑢 ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
97 96 nfcri ⊢ Ⅎ 𝑢 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
98 94 97 nfan ⊢ Ⅎ 𝑢 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
99 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
100 nfv ⊢ Ⅎ 𝑣 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
101 39 100 nfan ⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
102 nfv ⊢ Ⅎ 𝑣 𝑢 ∈ 𝑈
103 101 102 nfan ⊢ Ⅎ 𝑣 ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 )
104 nfv ⊢ Ⅎ 𝑣 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } )
105 103 104 nfan ⊢ Ⅎ 𝑣 ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
106 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
107 42 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑔 Fn 𝑉 )
108 fniniseg ⊢ ( 𝑔 Fn 𝑉 → ( 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = 𝑢 ) ) )
109 107 108 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = 𝑢 ) ) )
110 109 biimpa ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑣 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑣 ) = 𝑢 ) )
111 110 simpld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑣 ∈ 𝑉 )
112 rspa ⊢ ( ( ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
113 106 111 112 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) )
114 110 simprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑔 ‘ 𝑣 ) = 𝑢 )
115 113 114 sseqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑣 ⊆ 𝑢 )
116 115 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) → 𝑣 ⊆ 𝑢 ) )
117 105 116 ralrimi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∀ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑣 ⊆ 𝑢 )
118 unissb ⊢ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝑢 ↔ ∀ 𝑣 ∈ ( ◡ 𝑔 “ { 𝑢 } ) 𝑣 ⊆ 𝑢 )
119 117 118 sylibr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ∪ ( ◡ 𝑔 “ { 𝑢 } ) ⊆ 𝑢 )
120 99 119 eqsstrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → 𝑤 ⊆ 𝑢 )
121 120 exp31 ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ( 𝑢 ∈ 𝑈 → ( 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) → 𝑤 ⊆ 𝑢 ) ) )
122 98 121 reximdai ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑢 } ) → ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 ) )
123 93 122 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) → ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 )
124 123 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∀ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 )
125 vex ⊢ 𝑔 ∈ V
126 125 rnex ⊢ ran 𝑔 ∈ V
127 126 mptex ⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V
128 rnexg ⊢ ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V )
129 127 128 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V )
130 eqid ⊢ ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
131 130 33 isref ⊢ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ V → ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ↔ ( ∪ 𝑈 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ∀ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 ) ) )
132 129 131 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ↔ ( ∪ 𝑈 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ∀ 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∃ 𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢 ) ) )
133 86 124 132 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 )
134 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → 𝐽 ∈ Top )
135 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → 𝑋 = ∪ 𝑈 )
136 135 86 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → 𝑋 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
137 nfv ⊢ Ⅎ 𝑣 𝑥 ∈ 𝑋
138 39 137 nfan ⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 )
139 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) → 𝑣 ∈ 𝐽 )
140 ffun ⊢ ( 𝑔 : 𝑉 ⟶ 𝑈 → Fun 𝑔 )
141 140 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → Fun 𝑔 )
142 imafi ⊢ ( ( Fun 𝑔 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ∈ Fin )
143 141 142 sylancom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ∈ Fin )
144 simp3 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) )
145 sneq ⊢ ( 𝑢 = 𝑘 → { 𝑢 } = { 𝑘 } )
146 145 imaeq2d ⊢ ( 𝑢 = 𝑘 → ( ◡ 𝑔 “ { 𝑢 } ) = ( ◡ 𝑔 “ { 𝑘 } ) )
147 146 unieqd ⊢ ( 𝑢 = 𝑘 → ∪ ( ◡ 𝑔 “ { 𝑢 } ) = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
148 125 cnvex ⊢ ◡ 𝑔 ∈ V
149 imaexg ⊢ ( ◡ 𝑔 ∈ V → ( ◡ 𝑔 “ { 𝑘 } ) ∈ V )
150 148 149 ax-mp ⊢ ( ◡ 𝑔 “ { 𝑘 } ) ∈ V
151 150 uniex ⊢ ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∈ V
152 147 13 151 fvmpt ⊢ ( 𝑘 ∈ ran 𝑔 → ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
153 152 3ad2ant2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
154 144 153 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → 𝑤 = ∪ ( ◡ 𝑔 “ { 𝑘 } ) )
155 154 ineq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → ( 𝑤 ∩ 𝑣 ) = ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) )
156 155 neeq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ‘ 𝑘 ) ) → ( ( 𝑤 ∩ 𝑣 ) ≠ ∅ ↔ ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ ) )
157 126 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ran 𝑔 ∈ V )
158 imaexg ⊢ ( ◡ 𝑔 ∈ V → ( ◡ 𝑔 “ { 𝑢 } ) ∈ V )
159 148 158 ax-mp ⊢ ( ◡ 𝑔 “ { 𝑢 } ) ∈ V
160 159 uniex ⊢ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∈ V
161 160 13 fnmpti ⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Fn ran 𝑔
162 dffn4 ⊢ ( ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Fn ran 𝑔 ↔ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) : ran 𝑔 –onto→ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
163 161 162 mpbi ⊢ ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) : ran 𝑔 –onto→ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
164 163 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) : ran 𝑔 –onto→ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
165 156 157 164 rabfodom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑘 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ } )
166 sneq ⊢ ( 𝑘 = 𝑢 → { 𝑘 } = { 𝑢 } )
167 166 imaeq2d ⊢ ( 𝑘 = 𝑢 → ( ◡ 𝑔 “ { 𝑘 } ) = ( ◡ 𝑔 “ { 𝑢 } ) )
168 167 unieqd ⊢ ( 𝑘 = 𝑢 → ∪ ( ◡ 𝑔 “ { 𝑘 } ) = ∪ ( ◡ 𝑔 “ { 𝑢 } ) )
169 168 ineq1d ⊢ ( 𝑘 = 𝑢 → ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) = ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) )
170 169 neeq1d ⊢ ( 𝑘 = 𝑢 → ( ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ ↔ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) )
171 170 cbvrabv ⊢ { 𝑘 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑘 } ) ∩ 𝑣 ) ≠ ∅ } = { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ }
172 165 171 breqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } )
173 126 rabex ⊢ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ∈ V
174 nfv ⊢ Ⅎ 𝑗 ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 )
175 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ }
176 175 nfel1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin
177 174 176 nfan ⊢ Ⅎ 𝑗 ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin )
178 nfv ⊢ Ⅎ 𝑗 𝑢 ∈ ran 𝑔
179 177 178 nfan ⊢ Ⅎ 𝑗 ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 )
180 nfv ⊢ Ⅎ 𝑗 ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅
181 179 180 nfan ⊢ Ⅎ 𝑗 ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ )
182 nfv ⊢ Ⅎ 𝑗 ( 𝑔 ‘ 𝑘 ) = 𝑢
183 175 182 nfrexw ⊢ Ⅎ 𝑗 ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢
184 42 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑔 Fn 𝑉 )
185 184 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑔 Fn 𝑉 )
186 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) )
187 fniniseg ⊢ ( 𝑔 Fn 𝑉 → ( 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ↔ ( 𝑗 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) ) )
188 187 biimpa ⊢ ( ( 𝑔 Fn 𝑉 ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( 𝑗 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) )
189 185 186 188 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ( 𝑗 ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) )
190 189 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑗 ∈ 𝑉 )
191 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
192 rabid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ↔ ( 𝑗 ∈ 𝑉 ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) )
193 190 191 192 sylanbrc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → 𝑗 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } )
194 189 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ( 𝑔 ‘ 𝑗 ) = 𝑢 )
195 fveqeq2 ⊢ ( 𝑘 = 𝑗 → ( ( 𝑔 ‘ 𝑘 ) = 𝑢 ↔ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) )
196 195 rspcev ⊢ ( ( 𝑗 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∧ ( 𝑔 ‘ 𝑗 ) = 𝑢 ) → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 )
197 193 194 196 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) ∧ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ( 𝑗 ∩ 𝑣 ) ≠ ∅ ) → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 )
198 uniinn0 ⊢ ( ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ↔ ∃ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
199 198 biimpi ⊢ ( ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ → ∃ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
200 199 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) → ∃ 𝑗 ∈ ( ◡ 𝑔 “ { 𝑢 } ) ( 𝑗 ∩ 𝑣 ) ≠ ∅ )
201 181 183 197 200 r19.29af2 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) ∧ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ ) → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 )
202 201 ex ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ∧ 𝑢 ∈ ran 𝑔 ) → ( ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ → ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 ) )
203 202 ss2rabdv ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ⊆ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
204 ssdomg ⊢ ( { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ∈ V → ( { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ⊆ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } → { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ) )
205 173 203 204 mpsyl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
206 domtr ⊢ ( ( { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ∧ { 𝑢 ∈ ran 𝑔 ∣ ( ∪ ( ◡ 𝑔 “ { 𝑢 } ) ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
207 172 205 206 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
208 184 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → 𝑔 Fn 𝑉 )
209 dffn3 ⊢ ( 𝑔 Fn 𝑉 ↔ 𝑔 : 𝑉 ⟶ ran 𝑔 )
210 209 biimpi ⊢ ( 𝑔 Fn 𝑉 → 𝑔 : 𝑉 ⟶ ran 𝑔 )
211 ssrab2 ⊢ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ⊆ 𝑉
212 fimarab ⊢ ( ( 𝑔 : 𝑉 ⟶ ran 𝑔 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ⊆ 𝑉 ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) = { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
213 211 212 mpan2 ⊢ ( 𝑔 : 𝑉 ⟶ ran 𝑔 → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) = { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
214 208 210 213 3syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) = { 𝑢 ∈ ran 𝑔 ∣ ∃ 𝑘 ∈ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ( 𝑔 ‘ 𝑘 ) = 𝑢 } )
215 207 214 breqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) )
216 domfi ⊢ ( ( ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ∈ Fin ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ≼ ( 𝑔 “ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ) ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin )
217 143 215 216 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin )
218 217 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ( { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin → { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
219 218 imdistanda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) → ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
220 219 imp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) → ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
221 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
222 1 32 islocfin ⊢ ( 𝑉 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
223 6 222 sylib ⊢ ( 𝜑 → ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
224 223 simp3d ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
225 224 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
226 221 225 sylancom ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑗 ∈ 𝑉 ∣ ( 𝑗 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
227 138 139 220 226 reximd2a ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
228 227 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) )
229 1 130 islocfin ⊢ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ { 𝑤 ∈ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∣ ( 𝑤 ∩ 𝑣 ) ≠ ∅ } ∈ Fin ) ) )
230 134 136 228 229 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) )
231 funeq ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( Fun 𝑓 ↔ Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ) )
232 dmeq ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → dom 𝑓 = dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
233 232 sseq1d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( dom 𝑓 ⊆ 𝑈 ↔ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ) )
234 rneq ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ran 𝑓 = ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) )
235 234 sseq1d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ran 𝑓 ⊆ 𝐽 ↔ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) )
236 231 233 235 3anbi123d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ↔ ( Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) ) )
237 234 breq1d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ran 𝑓 Ref 𝑈 ↔ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ) )
238 234 eleq1d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ↔ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) )
239 237 238 anbi12d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ↔ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) )
240 236 239 anbi12d ⊢ ( 𝑓 = ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) → ( ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) ↔ ( ( Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) ∧ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) ) )
241 127 240 spcev ⊢ ( ( ( Fun ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∧ dom ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ⊆ 𝐽 ) ∧ ( ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) Ref 𝑈 ∧ ran ( 𝑢 ∈ ran 𝑔 ↦ ∪ ( ◡ 𝑔 “ { 𝑢 } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )
242 12 17 31 133 230 241 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑉 ⟶ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )
243 242 expl ⊢ ( 𝜑 → ( ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) ) )
244 243 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 : 𝑉 ⟶ 𝑈 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ⊆ ( 𝑔 ‘ 𝑣 ) ) → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) ) )
245 10 244 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽 ) ∧ ( ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )