Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  locfinreflem Structured version   Visualization version   GIF version
Theorem locfinreflem 32820
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. 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.)
Hypotheses
Ref Expression
locfinref.x 𝑋 = βˆͺ 𝐽
locfinref.1 (πœ‘ β†’ π‘ˆ βŠ† 𝐽)
locfinref.2 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
locfinref.3 (πœ‘ β†’ 𝑉 βŠ† 𝐽)
locfinref.4 (πœ‘ β†’ 𝑉Refπ‘ˆ)
locfinref.5 (πœ‘ β†’ 𝑉 ∈ (LocFinβ€˜π½))
Assertion
Ref Expression
locfinreflem (πœ‘ β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
Distinct variable groups:   𝑓,𝐽   π‘ˆ,𝑓   𝑓,𝑉   πœ‘,𝑓
Allowed substitution hint:   𝑋(𝑓)
Proof of Theorem locfinreflem
Dummy variables 𝑔 𝑗 π‘˜ 𝑒 𝑣 𝑀 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 locfinref.4 . . . 4 (πœ‘ β†’ 𝑉Refπ‘ˆ)
2 locfinref.5 . . . . 5 (πœ‘ β†’ 𝑉 ∈ (LocFinβ€˜π½))
3 reff 32819 . . . . 5 (𝑉 ∈ (LocFinβ€˜π½) β†’ (𝑉Refπ‘ˆ ↔ (βˆͺ π‘ˆ βŠ† βˆͺ 𝑉 ∧ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)))))
42, 3syl 17 . . . 4 (πœ‘ β†’ (𝑉Refπ‘ˆ ↔ (βˆͺ π‘ˆ βŠ† βˆͺ 𝑉 ∧ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)))))
51, 4mpbid 231 . . 3 (πœ‘ β†’ (βˆͺ π‘ˆ βŠ† βˆͺ 𝑉 ∧ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))))
65simprd 497 . 2 (πœ‘ β†’ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)))
7 funmpt 6587 . . . . . 6 Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
87a1i 11 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
9 eqid 2733 . . . . . . 7 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
109dmmptss 6241 . . . . . 6 dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† ran 𝑔
11 frn 6725 . . . . . . 7 (𝑔:π‘‰βŸΆπ‘ˆ β†’ ran 𝑔 βŠ† π‘ˆ)
1211ad2antlr 726 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran 𝑔 βŠ† π‘ˆ)
1310, 12sstrid 3994 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ)
14 locfintop 23025 . . . . . . . . . 10 (𝑉 ∈ (LocFinβ€˜π½) β†’ 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐽 ∈ Top)
1615ad3antrrr 729 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ 𝐽 ∈ Top)
17 cnvimass 6081 . . . . . . . . . 10 (◑𝑔 β€œ {𝑒}) βŠ† dom 𝑔
18 fdm 6727 . . . . . . . . . . 11 (𝑔:π‘‰βŸΆπ‘ˆ β†’ dom 𝑔 = 𝑉)
1918ad3antlr 730 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ dom 𝑔 = 𝑉)
2017, 19sseqtrid 4035 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ (◑𝑔 β€œ {𝑒}) βŠ† 𝑉)
21 locfinref.3 . . . . . . . . . 10 (πœ‘ β†’ 𝑉 βŠ† 𝐽)
2221ad3antrrr 729 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ 𝑉 βŠ† 𝐽)
2320, 22sstrd 3993 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ (◑𝑔 β€œ {𝑒}) βŠ† 𝐽)
24 uniopn 22399 . . . . . . . 8 ((𝐽 ∈ Top ∧ (◑𝑔 β€œ {𝑒}) βŠ† 𝐽) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽)
2516, 23, 24syl2anc 585 . . . . . . 7 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽)
2625ralrimiva 3147 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆ€π‘’ ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽)
279rnmptss 7122 . . . . . 6 (βˆ€π‘’ ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽 β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽)
2826, 27syl 17 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽)
29 eqid 2733 . . . . . . . . . 10 βˆͺ 𝑉 = βˆͺ 𝑉
30 eqid 2733 . . . . . . . . . 10 βˆͺ π‘ˆ = βˆͺ π‘ˆ
3129, 30refbas 23014 . . . . . . . . 9 (𝑉Refπ‘ˆ β†’ βˆͺ π‘ˆ = βˆͺ 𝑉)
321, 31syl 17 . . . . . . . 8 (πœ‘ β†’ βˆͺ π‘ˆ = βˆͺ 𝑉)
3332ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ π‘ˆ = βˆͺ 𝑉)
34 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑣(πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ)
35 nfra1 3282 . . . . . . . . . . . . 13 β„²π‘£βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)
3634, 35nfan 1903 . . . . . . . . . . . 12 Ⅎ𝑣((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))
37 nfre1 3283 . . . . . . . . . . . 12 β„²π‘£βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣
3836, 37nfan 1903 . . . . . . . . . . 11 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
39 ffn 6718 . . . . . . . . . . . . . . 15 (𝑔:π‘‰βŸΆπ‘ˆ β†’ 𝑔 Fn 𝑉)
4039ad4antlr 732 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ 𝑔 Fn 𝑉)
41 simplr 768 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ 𝑉)
42 fnfvelrn 7083 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) β†’ (π‘”β€˜π‘£) ∈ ran 𝑔)
4340, 41, 42syl2anc 585 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ (π‘”β€˜π‘£) ∈ ran 𝑔)
44 ssid 4005 . . . . . . . . . . . . . . 15 𝑣 βŠ† 𝑣
4539ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) β†’ 𝑔 Fn 𝑉)
46 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘”β€˜π‘£) = (π‘”β€˜π‘£)
47 fniniseg 7062 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 β†’ (𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}) ↔ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = (π‘”β€˜π‘£))))
4847biimpar 479 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = (π‘”β€˜π‘£))) β†’ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
4946, 48mpanr2 703 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5045, 49sylancom 589 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
51 ssuni 4937 . . . . . . . . . . . . . . 15 ((𝑣 βŠ† 𝑣 ∧ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)})) β†’ 𝑣 βŠ† βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5244, 50, 51sylancr 588 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 βŠ† βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5352sselda 3983 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
54 sneq 4639 . . . . . . . . . . . . . . . . 17 (𝑒 = (π‘”β€˜π‘£) β†’ {𝑒} = {(π‘”β€˜π‘£)})
5554imaeq2d 6060 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘”β€˜π‘£) β†’ (◑𝑔 β€œ {𝑒}) = (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5655unieqd 4923 . . . . . . . . . . . . . . 15 (𝑒 = (π‘”β€˜π‘£) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5756eleq2d 2820 . . . . . . . . . . . . . 14 (𝑒 = (π‘”β€˜π‘£) β†’ (π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}) ↔ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)})))
5857rspcev 3613 . . . . . . . . . . . . 13 (((π‘”β€˜π‘£) ∈ ran 𝑔 ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)})) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
5943, 53, 58syl2anc 585 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
6059adantllr 718 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
61 simpr 486 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣) β†’ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
6238, 60, 61r19.29af 3266 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
63 nfv 1918 . . . . . . . . . . . . . 14 Ⅎ𝑣 𝑒 ∈ ran 𝑔
6436, 63nfan 1903 . . . . . . . . . . . . 13 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔)
65 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑣 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})
6664, 65nfan 1903 . . . . . . . . . . . 12 Ⅎ𝑣((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
6720ad3antrrr 729 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ (◑𝑔 β€œ {𝑒}) βŠ† 𝑉)
68 simplr 768 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ (◑𝑔 β€œ {𝑒}))
6967, 68sseldd 3984 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ 𝑉)
70 simpr 486 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ 𝑣)
71 simpr 486 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
72 eluni2 4913 . . . . . . . . . . . . 13 (π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}) ↔ βˆƒπ‘£ ∈ (◑𝑔 β€œ {𝑒})π‘₯ ∈ 𝑣)
7371, 72sylib 217 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆƒπ‘£ ∈ (◑𝑔 β€œ {𝑒})π‘₯ ∈ 𝑣)
7466, 69, 70, 73reximd2a 3267 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
7574r19.29an 3159 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
7662, 75impbida 800 . . . . . . . . 9 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣 ↔ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})))
77 eluni2 4913 . . . . . . . . 9 (π‘₯ ∈ βˆͺ 𝑉 ↔ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
78 eliun 5002 . . . . . . . . 9 (π‘₯ ∈ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ↔ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
7976, 77, 783bitr4g 314 . . . . . . . 8 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (π‘₯ ∈ βˆͺ 𝑉 ↔ π‘₯ ∈ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒})))
8079eqrdv 2731 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ 𝑉 = βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}))
81 dfiun3g 5964 . . . . . . . 8 (βˆ€π‘’ ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽 β†’ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
8226, 81syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
8333, 80, 823eqtrd 2777 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ π‘ˆ = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
8411ad3antlr 730 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ ran 𝑔 βŠ† π‘ˆ)
85 vex 3479 . . . . . . . . . . 11 𝑀 ∈ V
869elrnmpt 5956 . . . . . . . . . . 11 (𝑀 ∈ V β†’ (𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ↔ βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})))
8785, 86mp1i 13 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ↔ βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})))
8887biimpa 478 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
89 ssrexv 4052 . . . . . . . . 9 (ran 𝑔 βŠ† π‘ˆ β†’ (βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})))
9084, 88, 89sylc 65 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
91 nfv 1918 . . . . . . . . . 10 Ⅎ𝑒((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))
92 nfmpt1 5257 . . . . . . . . . . . 12 Ⅎ𝑒(𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9392nfrn 5952 . . . . . . . . . . 11 Ⅎ𝑒ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9493nfcri 2891 . . . . . . . . . 10 Ⅎ𝑒 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9591, 94nfan 1903 . . . . . . . . 9 Ⅎ𝑒(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
96 simpr 486 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
97 nfv 1918 . . . . . . . . . . . . . . . 16 Ⅎ𝑣 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9836, 97nfan 1903 . . . . . . . . . . . . . . 15 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
99 nfv 1918 . . . . . . . . . . . . . . 15 Ⅎ𝑣 𝑒 ∈ π‘ˆ
10098, 99nfan 1903 . . . . . . . . . . . . . 14 Ⅎ𝑣((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ)
101 nfv 1918 . . . . . . . . . . . . . 14 Ⅎ𝑣 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})
102100, 101nfan 1903 . . . . . . . . . . . . 13 Ⅎ𝑣(((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
103 simp-5r 785 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))
10439ad5antlr 734 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ 𝑔 Fn 𝑉)
105 fniniseg 7062 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 β†’ (𝑣 ∈ (◑𝑔 β€œ {𝑒}) ↔ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = 𝑒)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (𝑣 ∈ (◑𝑔 β€œ {𝑒}) ↔ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = 𝑒)))
107106biimpa 478 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = 𝑒))
108107simpld 496 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ 𝑣 ∈ 𝑉)
109 rspa 3246 . . . . . . . . . . . . . . . 16 ((βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 βŠ† (π‘”β€˜π‘£))
110103, 108, 109syl2anc 585 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ 𝑣 βŠ† (π‘”β€˜π‘£))
111107simprd 497 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ (π‘”β€˜π‘£) = 𝑒)
112110, 111sseqtrd 4023 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ 𝑣 βŠ† 𝑒)
113112ex 414 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (𝑣 ∈ (◑𝑔 β€œ {𝑒}) β†’ 𝑣 βŠ† 𝑒))
114102, 113ralrimi 3255 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆ€π‘£ ∈ (◑𝑔 β€œ {𝑒})𝑣 βŠ† 𝑒)
115 unissb 4944 . . . . . . . . . . . 12 (βˆͺ (◑𝑔 β€œ {𝑒}) βŠ† 𝑒 ↔ βˆ€π‘£ ∈ (◑𝑔 β€œ {𝑒})𝑣 βŠ† 𝑒)
116114, 115sylibr 233 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) βŠ† 𝑒)
11796, 116eqsstrd 4021 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ 𝑀 βŠ† 𝑒)
118117exp31 421 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ (𝑒 ∈ π‘ˆ β†’ (𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}) β†’ 𝑀 βŠ† 𝑒)))
11995, 118reximdai 3259 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒))
12090, 119mpd 15 . . . . . . 7 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒)
121120ralrimiva 3147 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆ€π‘€ ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒)
122 vex 3479 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 7903 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 7225 . . . . . . . 8 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V
125 rnexg 7895 . . . . . . . 8 ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V)
127 eqid 2733 . . . . . . . 8 βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
128127, 30isref 23013 . . . . . . 7 (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V β†’ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ↔ (βˆͺ π‘ˆ = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ βˆ€π‘€ ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒)))
129126, 128syl 17 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ↔ (βˆͺ π‘ˆ = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ βˆ€π‘€ ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒)))
13083, 121, 129mpbir2and 712 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ)
13115ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
133132ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ 𝑋 = βˆͺ π‘ˆ)
134133, 83eqtrd 2773 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ 𝑋 = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
135 nfv 1918 . . . . . . . . 9 Ⅎ𝑣 π‘₯ ∈ 𝑋
13636, 135nfan 1903 . . . . . . . 8 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋)
137 simplr 768 . . . . . . . 8 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)) β†’ 𝑣 ∈ 𝐽)
138 ffun 6721 . . . . . . . . . . . . . 14 (𝑔:π‘‰βŸΆπ‘ˆ β†’ Fun 𝑔)
139138ad6antlr 736 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ Fun 𝑔)
140 imafi 9175 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) ∈ Fin)
141139, 140sylancom 589 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) ∈ Fin)
142 simp3 1139 . . . . . . . . . . . . . . . . . . 19 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜))
143 sneq 4639 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = π‘˜ β†’ {𝑒} = {π‘˜})
144143imaeq2d 6060 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = π‘˜ β†’ (◑𝑔 β€œ {𝑒}) = (◑𝑔 β€œ {π‘˜}))
145144unieqd 4923 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = π‘˜ β†’ βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ (◑𝑔 β€œ {π‘˜}))
146122cnvex 7916 . . . . . . . . . . . . . . . . . . . . . . 23 ◑𝑔 ∈ V
147 imaexg 7906 . . . . . . . . . . . . . . . . . . . . . . 23 (◑𝑔 ∈ V β†’ (◑𝑔 β€œ {π‘˜}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (◑𝑔 β€œ {π‘˜}) ∈ V
149148uniex 7731 . . . . . . . . . . . . . . . . . . . . 21 βˆͺ (◑𝑔 β€œ {π‘˜}) ∈ V
150145, 9, 149fvmpt 6999 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ ran 𝑔 β†’ ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜) = βˆͺ (◑𝑔 β€œ {π‘˜}))
1511503ad2ant2 1135 . . . . . . . . . . . . . . . . . . 19 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜) = βˆͺ (◑𝑔 β€œ {π‘˜}))
152142, 151eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ 𝑀 = βˆͺ (◑𝑔 β€œ {π‘˜}))
153152ineq1d 4212 . . . . . . . . . . . . . . . . 17 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ (𝑀 ∩ 𝑣) = (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣))
154153neeq1d 3001 . . . . . . . . . . . . . . . 16 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ ((𝑀 ∩ 𝑣) β‰  βˆ… ↔ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ…))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ ran 𝑔 ∈ V)
156 imaexg 7906 . . . . . . . . . . . . . . . . . . . . 21 (◑𝑔 ∈ V β†’ (◑𝑔 β€œ {𝑒}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (◑𝑔 β€œ {𝑒}) ∈ V
158157uniex 7731 . . . . . . . . . . . . . . . . . . 19 βˆͺ (◑𝑔 β€œ {𝑒}) ∈ V
159158, 9fnmpti 6694 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) Fn ran 𝑔
160 dffn4 6812 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) Fn ran 𝑔 ↔ (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})):ran 𝑔–ontoβ†’ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
161159, 160mpbi 229 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})):ran 𝑔–ontoβ†’ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
162161a1i 11 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})):ran 𝑔–ontoβ†’ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
163154, 155, 162rabfodom 31743 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {π‘˜ ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ…})
164 sneq 4639 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑒 β†’ {π‘˜} = {𝑒})
165164imaeq2d 6060 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑒 β†’ (◑𝑔 β€œ {π‘˜}) = (◑𝑔 β€œ {𝑒}))
166165unieqd 4923 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ βˆͺ (◑𝑔 β€œ {π‘˜}) = βˆͺ (◑𝑔 β€œ {𝑒}))
167166ineq1d 4212 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑒 β†’ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) = (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣))
168167neeq1d 3001 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑒 β†’ ((βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ… ↔ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…))
169168cbvrabv 3443 . . . . . . . . . . . . . . 15 {π‘˜ ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ…} = {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…}
170163, 169breqtrdi 5190 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…})
171123rabex 5333 . . . . . . . . . . . . . . 15 {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒} ∈ V
172 nfv 1918 . . . . . . . . . . . . . . . . . . . . 21 Ⅎ𝑗(((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣)
173 nfrab1 3452 . . . . . . . . . . . . . . . . . . . . . 22 Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}
174173nfel1 2920 . . . . . . . . . . . . . . . . . . . . 21 Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin
175172, 174nfan 1903 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)
176 nfv 1918 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗 𝑒 ∈ ran 𝑔
177175, 176nfan 1903 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔)
178 nfv 1918 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…
179177, 178nfan 1903 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…)
180 nfv 1918 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(π‘”β€˜π‘˜) = 𝑒
181173, 180nfrexw 3311 . . . . . . . . . . . . . . . . . 18 β„²π‘—βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒
18239ad5antlr 734 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) β†’ 𝑔 Fn 𝑉)
183182ad5antr 733 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑔 Fn 𝑉)
184 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑗 ∈ (◑𝑔 β€œ {𝑒}))
185 fniniseg 7062 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 β†’ (𝑗 ∈ (◑𝑔 β€œ {𝑒}) ↔ (𝑗 ∈ 𝑉 ∧ (π‘”β€˜π‘—) = 𝑒)))
186185biimpa 478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) β†’ (𝑗 ∈ 𝑉 ∧ (π‘”β€˜π‘—) = 𝑒))
187183, 184, 186syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ (𝑗 ∈ 𝑉 ∧ (π‘”β€˜π‘—) = 𝑒))
188187simpld 496 . . . . . . . . . . . . . . . . . . . 20 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑗 ∈ 𝑉)
189 simpr 486 . . . . . . . . . . . . . . . . . . . 20 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ (𝑗 ∩ 𝑣) β‰  βˆ…)
190 rabid 3453 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) β‰  βˆ…))
191188, 189, 190sylanbrc 584 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…})
192187simprd 497 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ (π‘”β€˜π‘—) = 𝑒)
193 fveqeq2 6901 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑗 β†’ ((π‘”β€˜π‘˜) = 𝑒 ↔ (π‘”β€˜π‘—) = 𝑒))
194193rspcev 3613 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∧ (π‘”β€˜π‘—) = 𝑒) β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒)
195191, 192, 194syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒)
196 uniinn0 31782 . . . . . . . . . . . . . . . . . . . 20 ((βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ… ↔ βˆƒπ‘— ∈ (◑𝑔 β€œ {𝑒})(𝑗 ∩ 𝑣) β‰  βˆ…)
197196biimpi 215 . . . . . . . . . . . . . . . . . . 19 ((βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ… β†’ βˆƒπ‘— ∈ (◑𝑔 β€œ {𝑒})(𝑗 ∩ 𝑣) β‰  βˆ…)
198197adantl 483 . . . . . . . . . . . . . . . . . 18 (((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) β†’ βˆƒπ‘— ∈ (◑𝑔 β€œ {𝑒})(𝑗 ∩ 𝑣) β‰  βˆ…)
199179, 181, 195, 198r19.29af2 3265 . . . . . . . . . . . . . . . . 17 (((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒)
200199ex 414 . . . . . . . . . . . . . . . 16 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) β†’ ((βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒))
201200ss2rabdv 4074 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} βŠ† {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
202 ssdomg 8996 . . . . . . . . . . . . . . 15 ({𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒} ∈ V β†’ ({𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} βŠ† {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒} β†’ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒}))
203171, 201, 202mpsyl 68 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
204 domtr 9003 . . . . . . . . . . . . . 14 (({𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} ∧ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒}) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
205170, 203, 204syl2anc 585 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
206182adantr 482 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ 𝑔 Fn 𝑉)
207 dffn3 6731 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉 ↔ 𝑔:π‘‰βŸΆran 𝑔)
208207biimpi 215 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉 β†’ 𝑔:π‘‰βŸΆran 𝑔)
209 ssrab2 4078 . . . . . . . . . . . . . . 15 {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} βŠ† 𝑉
210 fimarab 31868 . . . . . . . . . . . . . . 15 ((𝑔:π‘‰βŸΆran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} βŠ† 𝑉) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) = {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
211209, 210mpan2 690 . . . . . . . . . . . . . 14 (𝑔:π‘‰βŸΆran 𝑔 β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) = {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
212206, 208, 2113syl 18 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) = {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
213205, 212breqtrrd 5177 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}))
214 domfi 9192 . . . . . . . . . . . 12 (((𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) ∈ Fin ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…})) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)
215141, 213, 214syl2anc 585 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)
216215ex 414 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) β†’ ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
217216imdistanda 573 . . . . . . . . 9 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) β†’ ((π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
218217imp 408 . . . . . . . 8 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)) β†’ (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
219 simplll 774 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) β†’ πœ‘)
220 locfinref.x . . . . . . . . . . . . 13 𝑋 = βˆͺ 𝐽
221220, 29islocfin 23021 . . . . . . . . . . . 12 (𝑉 ∈ (LocFinβ€˜π½) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝑉 ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
2222, 221sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝑉 ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
223222simp3d 1145 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
224223r19.21bi 3249 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
225219, 224sylancom 589 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
226136, 137, 218, 225reximd2a 3267 . . . . . . 7 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
227226ralrimiva 3147 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
228220, 127islocfin 23021 . . . . . 6 (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
229131, 134, 227, 228syl3anbrc 1344 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½))
230 funeq 6569 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (Fun 𝑓 ↔ Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))))
231 dmeq 5904 . . . . . . . . 9 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ dom 𝑓 = dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
232231sseq1d 4014 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (dom 𝑓 βŠ† π‘ˆ ↔ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ))
233 rneq 5936 . . . . . . . . 9 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ ran 𝑓 = ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
234233sseq1d 4014 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (ran 𝑓 βŠ† 𝐽 ↔ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽))
235230, 232, 2343anbi123d 1437 . . . . . . 7 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ ((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ↔ (Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽)))
236233breq1d 5159 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (ran 𝑓Refπ‘ˆ ↔ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ))
237233eleq1d 2819 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (ran 𝑓 ∈ (LocFinβ€˜π½) ↔ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½)))
238236, 237anbi12d 632 . . . . . . 7 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ ((ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)) ↔ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½))))
239235, 238anbi12d 632 . . . . . 6 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))) ↔ ((Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽) ∧ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½)))))
240124, 239spcev 3597 . . . . 5 (((Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽) ∧ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½))) β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
2418, 13, 28, 130, 229, 240syl32anc 1379 . . . 4 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
242241expl 459 . . 3 (πœ‘ β†’ ((𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))))
243242exlimdv 1937 . 2 (πœ‘ β†’ (βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))))
2446, 243mpd 15 1 (πœ‘ β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  {csn 4629  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β€œ cima 5680  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544   β‰Ό cdom 8937  Fincfn 8939  Topctop 22395  Refcref 23006  LocFinclocfin 23008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-reg 9587  ax-inf2 9636  ax-ac2 10458
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-fin 8943  df-r1 9759  df-rank 9760  df-card 9934  df-ac 10111  df-top 22396  df-ref 23009  df-locfin 23011
This theorem is referenced by:  locfinref  32821
  Copyright terms: Public domain W3C validator