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 33118
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 33117 . . . . 5 (𝑉 ∈ (LocFinβ€˜π½) β†’ (𝑉Refπ‘ˆ ↔ (βˆͺ π‘ˆ βŠ† βˆͺ 𝑉 ∧ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)))))
42, 3syl 17 . . . 4 (πœ‘ β†’ (𝑉Refπ‘ˆ ↔ (βˆͺ π‘ˆ βŠ† βˆͺ 𝑉 ∧ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)))))
51, 4mpbid 231 . . 3 (πœ‘ β†’ (βˆͺ π‘ˆ βŠ† βˆͺ 𝑉 ∧ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))))
65simprd 494 . 2 (πœ‘ β†’ βˆƒπ‘”(𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)))
7 funmpt 6585 . . . . . 6 Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
87a1i 11 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
9 eqid 2730 . . . . . . 7 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
109dmmptss 6239 . . . . . 6 dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† ran 𝑔
11 frn 6723 . . . . . . 7 (𝑔:π‘‰βŸΆπ‘ˆ β†’ ran 𝑔 βŠ† π‘ˆ)
1211ad2antlr 723 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran 𝑔 βŠ† π‘ˆ)
1310, 12sstrid 3992 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ)
14 locfintop 23245 . . . . . . . . . 10 (𝑉 ∈ (LocFinβ€˜π½) β†’ 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐽 ∈ Top)
1615ad3antrrr 726 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ 𝐽 ∈ Top)
17 cnvimass 6079 . . . . . . . . . 10 (◑𝑔 β€œ {𝑒}) βŠ† dom 𝑔
18 fdm 6725 . . . . . . . . . . 11 (𝑔:π‘‰βŸΆπ‘ˆ β†’ dom 𝑔 = 𝑉)
1918ad3antlr 727 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ dom 𝑔 = 𝑉)
2017, 19sseqtrid 4033 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ (◑𝑔 β€œ {𝑒}) βŠ† 𝑉)
21 locfinref.3 . . . . . . . . . 10 (πœ‘ β†’ 𝑉 βŠ† 𝐽)
2221ad3antrrr 726 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ 𝑉 βŠ† 𝐽)
2320, 22sstrd 3991 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ (◑𝑔 β€œ {𝑒}) βŠ† 𝐽)
24 uniopn 22619 . . . . . . . 8 ((𝐽 ∈ Top ∧ (◑𝑔 β€œ {𝑒}) βŠ† 𝐽) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽)
2516, 23, 24syl2anc 582 . . . . . . 7 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽)
2625ralrimiva 3144 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆ€π‘’ ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽)
279rnmptss 7123 . . . . . 6 (βˆ€π‘’ ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽 β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽)
2826, 27syl 17 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽)
29 eqid 2730 . . . . . . . . . 10 βˆͺ 𝑉 = βˆͺ 𝑉
30 eqid 2730 . . . . . . . . . 10 βˆͺ π‘ˆ = βˆͺ π‘ˆ
3129, 30refbas 23234 . . . . . . . . 9 (𝑉Refπ‘ˆ β†’ βˆͺ π‘ˆ = βˆͺ 𝑉)
321, 31syl 17 . . . . . . . 8 (πœ‘ β†’ βˆͺ π‘ˆ = βˆͺ 𝑉)
3332ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ π‘ˆ = βˆͺ 𝑉)
34 nfv 1915 . . . . . . . . . . . . 13 Ⅎ𝑣(πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ)
35 nfra1 3279 . . . . . . . . . . . . 13 β„²π‘£βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)
3634, 35nfan 1900 . . . . . . . . . . . 12 Ⅎ𝑣((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))
37 nfre1 3280 . . . . . . . . . . . 12 β„²π‘£βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣
3836, 37nfan 1900 . . . . . . . . . . 11 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
39 ffn 6716 . . . . . . . . . . . . . . 15 (𝑔:π‘‰βŸΆπ‘ˆ β†’ 𝑔 Fn 𝑉)
4039ad4antlr 729 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ 𝑔 Fn 𝑉)
41 simplr 765 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ 𝑉)
42 fnfvelrn 7081 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) β†’ (π‘”β€˜π‘£) ∈ ran 𝑔)
4340, 41, 42syl2anc 582 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ (π‘”β€˜π‘£) ∈ ran 𝑔)
44 ssid 4003 . . . . . . . . . . . . . . 15 𝑣 βŠ† 𝑣
4539ad3antlr 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) β†’ 𝑔 Fn 𝑉)
46 eqid 2730 . . . . . . . . . . . . . . . . 17 (π‘”β€˜π‘£) = (π‘”β€˜π‘£)
47 fniniseg 7060 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 β†’ (𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}) ↔ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = (π‘”β€˜π‘£))))
4847biimpar 476 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = (π‘”β€˜π‘£))) β†’ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
4946, 48mpanr2 700 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5045, 49sylancom 586 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
51 ssuni 4935 . . . . . . . . . . . . . . 15 ((𝑣 βŠ† 𝑣 ∧ 𝑣 ∈ (◑𝑔 β€œ {(π‘”β€˜π‘£)})) β†’ 𝑣 βŠ† βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5244, 50, 51sylancr 585 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 βŠ† βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5352sselda 3981 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
54 sneq 4637 . . . . . . . . . . . . . . . . 17 (𝑒 = (π‘”β€˜π‘£) β†’ {𝑒} = {(π‘”β€˜π‘£)})
5554imaeq2d 6058 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘”β€˜π‘£) β†’ (◑𝑔 β€œ {𝑒}) = (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5655unieqd 4921 . . . . . . . . . . . . . . 15 (𝑒 = (π‘”β€˜π‘£) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)}))
5756eleq2d 2817 . . . . . . . . . . . . . 14 (𝑒 = (π‘”β€˜π‘£) β†’ (π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}) ↔ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)})))
5857rspcev 3611 . . . . . . . . . . . . 13 (((π‘”β€˜π‘£) ∈ ran 𝑔 ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {(π‘”β€˜π‘£)})) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
5943, 53, 58syl2anc 582 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
6059adantllr 715 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ π‘₯ ∈ 𝑣) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
61 simpr 483 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣) β†’ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
6238, 60, 61r19.29af 3263 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣) β†’ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
63 nfv 1915 . . . . . . . . . . . . . 14 Ⅎ𝑣 𝑒 ∈ ran 𝑔
6436, 63nfan 1900 . . . . . . . . . . . . 13 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔)
65 nfv 1915 . . . . . . . . . . . . 13 Ⅎ𝑣 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})
6664, 65nfan 1900 . . . . . . . . . . . 12 Ⅎ𝑣((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
6720ad3antrrr 726 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ (◑𝑔 β€œ {𝑒}) βŠ† 𝑉)
68 simplr 765 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ (◑𝑔 β€œ {𝑒}))
6967, 68sseldd 3982 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ 𝑉)
70 simpr 483 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ 𝑣)
71 simpr 483 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
72 eluni2 4911 . . . . . . . . . . . . 13 (π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}) ↔ βˆƒπ‘£ ∈ (◑𝑔 β€œ {𝑒})π‘₯ ∈ 𝑣)
7371, 72sylib 217 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆƒπ‘£ ∈ (◑𝑔 β€œ {𝑒})π‘₯ ∈ 𝑣)
7466, 69, 70, 73reximd2a 3264 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑒 ∈ ran 𝑔) ∧ π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
7574r19.29an 3156 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
7662, 75impbida 797 . . . . . . . . 9 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣 ↔ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒})))
77 eluni2 4911 . . . . . . . . 9 (π‘₯ ∈ βˆͺ 𝑉 ↔ βˆƒπ‘£ ∈ 𝑉 π‘₯ ∈ 𝑣)
78 eliun 5000 . . . . . . . . 9 (π‘₯ ∈ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ↔ βˆƒπ‘’ ∈ ran 𝑔 π‘₯ ∈ βˆͺ (◑𝑔 β€œ {𝑒}))
7976, 77, 783bitr4g 313 . . . . . . . 8 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (π‘₯ ∈ βˆͺ 𝑉 ↔ π‘₯ ∈ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒})))
8079eqrdv 2728 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ 𝑉 = βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}))
81 dfiun3g 5962 . . . . . . . 8 (βˆ€π‘’ ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) ∈ 𝐽 β†’ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
8226, 81syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ 𝑒 ∈ ran 𝑔βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
8333, 80, 823eqtrd 2774 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆͺ π‘ˆ = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
8411ad3antlr 727 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ ran 𝑔 βŠ† π‘ˆ)
85 vex 3476 . . . . . . . . . . 11 𝑀 ∈ V
869elrnmpt 5954 . . . . . . . . . . 11 (𝑀 ∈ V β†’ (𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ↔ βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})))
8785, 86mp1i 13 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ (𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ↔ βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})))
8887biimpa 475 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
89 ssrexv 4050 . . . . . . . . 9 (ran 𝑔 βŠ† π‘ˆ β†’ (βˆƒπ‘’ ∈ ran 𝑔 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})))
9084, 88, 89sylc 65 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
91 nfv 1915 . . . . . . . . . 10 Ⅎ𝑒((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))
92 nfmpt1 5255 . . . . . . . . . . . 12 Ⅎ𝑒(𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9392nfrn 5950 . . . . . . . . . . 11 Ⅎ𝑒ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9493nfcri 2888 . . . . . . . . . 10 Ⅎ𝑒 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9591, 94nfan 1900 . . . . . . . . 9 Ⅎ𝑒(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
96 simpr 483 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
97 nfv 1915 . . . . . . . . . . . . . . . 16 Ⅎ𝑣 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
9836, 97nfan 1900 . . . . . . . . . . . . . . 15 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
99 nfv 1915 . . . . . . . . . . . . . . 15 Ⅎ𝑣 𝑒 ∈ π‘ˆ
10098, 99nfan 1900 . . . . . . . . . . . . . 14 Ⅎ𝑣((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ)
101 nfv 1915 . . . . . . . . . . . . . 14 Ⅎ𝑣 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})
102100, 101nfan 1900 . . . . . . . . . . . . 13 Ⅎ𝑣(((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}))
103 simp-5r 782 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£))
10439ad5antlr 731 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ 𝑔 Fn 𝑉)
105 fniniseg 7060 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 β†’ (𝑣 ∈ (◑𝑔 β€œ {𝑒}) ↔ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = 𝑒)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (𝑣 ∈ (◑𝑔 β€œ {𝑒}) ↔ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = 𝑒)))
107106biimpa 475 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ (𝑣 ∈ 𝑉 ∧ (π‘”β€˜π‘£) = 𝑒))
108107simpld 493 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ 𝑣 ∈ 𝑉)
109 rspa 3243 . . . . . . . . . . . . . . . 16 ((βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 βŠ† (π‘”β€˜π‘£))
110103, 108, 109syl2anc 582 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ 𝑣 βŠ† (π‘”β€˜π‘£))
111107simprd 494 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ (π‘”β€˜π‘£) = 𝑒)
112110, 111sseqtrd 4021 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) ∧ 𝑣 ∈ (◑𝑔 β€œ {𝑒})) β†’ 𝑣 βŠ† 𝑒)
113112ex 411 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (𝑣 ∈ (◑𝑔 β€œ {𝑒}) β†’ 𝑣 βŠ† 𝑒))
114102, 113ralrimi 3252 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆ€π‘£ ∈ (◑𝑔 β€œ {𝑒})𝑣 βŠ† 𝑒)
115 unissb 4942 . . . . . . . . . . . 12 (βˆͺ (◑𝑔 β€œ {𝑒}) βŠ† 𝑒 ↔ βˆ€π‘£ ∈ (◑𝑔 β€œ {𝑒})𝑣 βŠ† 𝑒)
116114, 115sylibr 233 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ βˆͺ (◑𝑔 β€œ {𝑒}) βŠ† 𝑒)
11796, 116eqsstrd 4019 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒})) β†’ 𝑀 βŠ† 𝑒)
118117exp31 418 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ (𝑒 ∈ π‘ˆ β†’ (𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}) β†’ 𝑀 βŠ† 𝑒)))
11995, 118reximdai 3256 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = βˆͺ (◑𝑔 β€œ {𝑒}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒))
12090, 119mpd 15 . . . . . . 7 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ 𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒)
121120ralrimiva 3144 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆ€π‘€ ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))βˆƒπ‘’ ∈ π‘ˆ 𝑀 βŠ† 𝑒)
122 vex 3476 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 7905 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 7226 . . . . . . . 8 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V
125 rnexg 7897 . . . . . . . 8 ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ V)
127 eqid 2730 . . . . . . . 8 βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))
128127, 30isref 23233 . . . . . . 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 709 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ)
13115ad2antrr 722 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
133132ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ 𝑋 = βˆͺ π‘ˆ)
134133, 83eqtrd 2770 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ 𝑋 = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
135 nfv 1915 . . . . . . . . 9 Ⅎ𝑣 π‘₯ ∈ 𝑋
13636, 135nfan 1900 . . . . . . . 8 Ⅎ𝑣(((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋)
137 simplr 765 . . . . . . . 8 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)) β†’ 𝑣 ∈ 𝐽)
138 ffun 6719 . . . . . . . . . . . . . 14 (𝑔:π‘‰βŸΆπ‘ˆ β†’ Fun 𝑔)
139138ad6antlr 733 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ Fun 𝑔)
140 imafi 9177 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) ∈ Fin)
141139, 140sylancom 586 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) ∈ Fin)
142 simp3 1136 . . . . . . . . . . . . . . . . . . 19 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜))
143 sneq 4637 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = π‘˜ β†’ {𝑒} = {π‘˜})
144143imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = π‘˜ β†’ (◑𝑔 β€œ {𝑒}) = (◑𝑔 β€œ {π‘˜}))
145144unieqd 4921 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = π‘˜ β†’ βˆͺ (◑𝑔 β€œ {𝑒}) = βˆͺ (◑𝑔 β€œ {π‘˜}))
146122cnvex 7918 . . . . . . . . . . . . . . . . . . . . . . 23 ◑𝑔 ∈ V
147 imaexg 7908 . . . . . . . . . . . . . . . . . . . . . . 23 (◑𝑔 ∈ V β†’ (◑𝑔 β€œ {π‘˜}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (◑𝑔 β€œ {π‘˜}) ∈ V
149148uniex 7733 . . . . . . . . . . . . . . . . . . . . 21 βˆͺ (◑𝑔 β€œ {π‘˜}) ∈ V
150145, 9, 149fvmpt 6997 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ ran 𝑔 β†’ ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜) = βˆͺ (◑𝑔 β€œ {π‘˜}))
1511503ad2ant2 1132 . . . . . . . . . . . . . . . . . . 19 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜) = βˆͺ (◑𝑔 β€œ {π‘˜}))
152142, 151eqtrd 2770 . . . . . . . . . . . . . . . . . 18 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ 𝑀 = βˆͺ (◑𝑔 β€œ {π‘˜}))
153152ineq1d 4210 . . . . . . . . . . . . . . . . 17 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ (𝑀 ∩ 𝑣) = (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣))
154153neeq1d 2998 . . . . . . . . . . . . . . . 16 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ π‘˜ ∈ ran 𝑔 ∧ 𝑀 = ((𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))β€˜π‘˜)) β†’ ((𝑀 ∩ 𝑣) β‰  βˆ… ↔ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ…))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ ran 𝑔 ∈ V)
156 imaexg 7908 . . . . . . . . . . . . . . . . . . . . 21 (◑𝑔 ∈ V β†’ (◑𝑔 β€œ {𝑒}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (◑𝑔 β€œ {𝑒}) ∈ V
158157uniex 7733 . . . . . . . . . . . . . . . . . . 19 βˆͺ (◑𝑔 β€œ {𝑒}) ∈ V
159158, 9fnmpti 6692 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) Fn ran 𝑔
160 dffn4 6810 . . . . . . . . . . . . . . . . . 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 32010 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {π‘˜ ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ…})
164 sneq 4637 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑒 β†’ {π‘˜} = {𝑒})
165164imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑒 β†’ (◑𝑔 β€œ {π‘˜}) = (◑𝑔 β€œ {𝑒}))
166165unieqd 4921 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑒 β†’ βˆͺ (◑𝑔 β€œ {π‘˜}) = βˆͺ (◑𝑔 β€œ {𝑒}))
167166ineq1d 4210 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑒 β†’ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) = (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣))
168167neeq1d 2998 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑒 β†’ ((βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ… ↔ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…))
169168cbvrabv 3440 . . . . . . . . . . . . . . 15 {π‘˜ ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {π‘˜}) ∩ 𝑣) β‰  βˆ…} = {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…}
170163, 169breqtrdi 5188 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…})
171123rabex 5331 . . . . . . . . . . . . . . 15 {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒} ∈ V
172 nfv 1915 . . . . . . . . . . . . . . . . . . . . 21 Ⅎ𝑗(((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣)
173 nfrab1 3449 . . . . . . . . . . . . . . . . . . . . . 22 Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}
174173nfel1 2917 . . . . . . . . . . . . . . . . . . . . 21 Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin
175172, 174nfan 1900 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)
176 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗 𝑒 ∈ ran 𝑔
177175, 176nfan 1900 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔)
178 nfv 1915 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…
179177, 178nfan 1900 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…)
180 nfv 1915 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(π‘”β€˜π‘˜) = 𝑒
181173, 180nfrexw 3308 . . . . . . . . . . . . . . . . . 18 β„²π‘—βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒
18239ad5antlr 731 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) β†’ 𝑔 Fn 𝑉)
183182ad5antr 730 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑔 Fn 𝑉)
184 simplr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑗 ∈ (◑𝑔 β€œ {𝑒}))
185 fniniseg 7060 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 β†’ (𝑗 ∈ (◑𝑔 β€œ {𝑒}) ↔ (𝑗 ∈ 𝑉 ∧ (π‘”β€˜π‘—) = 𝑒)))
186185biimpa 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) β†’ (𝑗 ∈ 𝑉 ∧ (π‘”β€˜π‘—) = 𝑒))
187183, 184, 186syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ (𝑗 ∈ 𝑉 ∧ (π‘”β€˜π‘—) = 𝑒))
188187simpld 493 . . . . . . . . . . . . . . . . . . . 20 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑗 ∈ 𝑉)
189 simpr 483 . . . . . . . . . . . . . . . . . . . 20 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ (𝑗 ∩ 𝑣) β‰  βˆ…)
190 rabid 3450 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) β‰  βˆ…))
191188, 189, 190sylanbrc 581 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…})
192187simprd 494 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ (π‘”β€˜π‘—) = 𝑒)
193 fveqeq2 6899 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑗 β†’ ((π‘”β€˜π‘˜) = 𝑒 ↔ (π‘”β€˜π‘—) = 𝑒))
194193rspcev 3611 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∧ (π‘”β€˜π‘—) = 𝑒) β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒)
195191, 192, 194syl2anc 582 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) ∧ 𝑗 ∈ (◑𝑔 β€œ {𝑒})) ∧ (𝑗 ∩ 𝑣) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒)
196 uniinn0 32049 . . . . . . . . . . . . . . . . . . . 20 ((βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ… ↔ βˆƒπ‘— ∈ (◑𝑔 β€œ {𝑒})(𝑗 ∩ 𝑣) β‰  βˆ…)
197196biimpi 215 . . . . . . . . . . . . . . . . . . 19 ((βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ… β†’ βˆƒπ‘— ∈ (◑𝑔 β€œ {𝑒})(𝑗 ∩ 𝑣) β‰  βˆ…)
198197adantl 480 . . . . . . . . . . . . . . . . . 18 (((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) β†’ βˆƒπ‘— ∈ (◑𝑔 β€œ {𝑒})(𝑗 ∩ 𝑣) β‰  βˆ…)
199179, 181, 195, 198r19.29af2 3262 . . . . . . . . . . . . . . . . 17 (((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) ∧ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒)
200199ex 411 . . . . . . . . . . . . . . . 16 ((((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) ∧ 𝑒 ∈ ran 𝑔) β†’ ((βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒))
201200ss2rabdv 4072 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} βŠ† {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
202 ssdomg 8998 . . . . . . . . . . . . . . 15 ({𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒} ∈ V β†’ ({𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} βŠ† {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒} β†’ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒}))
203171, 201, 202mpsyl 68 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
204 domtr 9005 . . . . . . . . . . . . . 14 (({𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} ∧ {𝑒 ∈ ran 𝑔 ∣ (βˆͺ (◑𝑔 β€œ {𝑒}) ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒}) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
205170, 203, 204syl2anc 582 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
206182adantr 479 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ 𝑔 Fn 𝑉)
207 dffn3 6729 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉 ↔ 𝑔:π‘‰βŸΆran 𝑔)
208207biimpi 215 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉 β†’ 𝑔:π‘‰βŸΆran 𝑔)
209 ssrab2 4076 . . . . . . . . . . . . . . 15 {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} βŠ† 𝑉
210 fimarab 32135 . . . . . . . . . . . . . . 15 ((𝑔:π‘‰βŸΆran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} βŠ† 𝑉) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) = {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
211209, 210mpan2 687 . . . . . . . . . . . . . 14 (𝑔:π‘‰βŸΆran 𝑔 β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) = {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
212206, 208, 2113syl 18 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) = {𝑒 ∈ ran 𝑔 ∣ βˆƒπ‘˜ ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} (π‘”β€˜π‘˜) = 𝑒})
213205, 212breqtrrd 5175 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}))
214 domfi 9194 . . . . . . . . . . . 12 (((𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…}) ∈ Fin ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} β‰Ό (𝑔 β€œ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…})) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)
215141, 213, 214syl2anc 582 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)
216215ex 411 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ π‘₯ ∈ 𝑣) β†’ ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin β†’ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
217216imdistanda 570 . . . . . . . . 9 (((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) β†’ ((π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin) β†’ (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
218217imp 405 . . . . . . . 8 ((((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)) β†’ (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
219 simplll 771 . . . . . . . . 9 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) β†’ πœ‘)
220 locfinref.x . . . . . . . . . . . . 13 𝑋 = βˆͺ 𝐽
221220, 29islocfin 23241 . . . . . . . . . . . 12 (𝑉 ∈ (LocFinβ€˜π½) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝑉 ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
2222, 221sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝑉 ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
223222simp3d 1142 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
224223r19.21bi 3246 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
225219, 224sylancom 586 . . . . . . . 8 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
226136, 137, 218, 225reximd2a 3264 . . . . . . 7 ((((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) ∧ π‘₯ ∈ 𝑋) β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
227226ralrimiva 3144 . . . . . 6 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin))
228220, 127islocfin 23241 . . . . . 6 (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ {𝑀 ∈ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∣ (𝑀 ∩ 𝑣) β‰  βˆ…} ∈ Fin)))
229131, 134, 227, 228syl3anbrc 1341 . . . . 5 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½))
230 funeq 6567 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (Fun 𝑓 ↔ Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))))
231 dmeq 5902 . . . . . . . . 9 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ dom 𝑓 = dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
232231sseq1d 4012 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (dom 𝑓 βŠ† π‘ˆ ↔ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ))
233 rneq 5934 . . . . . . . . 9 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ ran 𝑓 = ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})))
234233sseq1d 4012 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (ran 𝑓 βŠ† 𝐽 ↔ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽))
235230, 232, 2343anbi123d 1434 . . . . . . 7 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ ((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ↔ (Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽)))
236233breq1d 5157 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (ran 𝑓Refπ‘ˆ ↔ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ))
237233eleq1d 2816 . . . . . . . 8 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (ran 𝑓 ∈ (LocFinβ€˜π½) ↔ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½)))
238236, 237anbi12d 629 . . . . . . 7 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ ((ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)) ↔ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½))))
239235, 238anbi12d 629 . . . . . 6 (𝑓 = (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) β†’ (((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))) ↔ ((Fun (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∧ dom (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† π‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) βŠ† 𝐽) ∧ (ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒}))Refπ‘ˆ ∧ ran (𝑒 ∈ ran 𝑔 ↦ βˆͺ (◑𝑔 β€œ {𝑒})) ∈ (LocFinβ€˜π½)))))
240124, 239spcev 3595 . . . . 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 1376 . . . 4 (((πœ‘ ∧ 𝑔:π‘‰βŸΆπ‘ˆ) ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
242241expl 456 . . 3 (πœ‘ β†’ ((𝑔:π‘‰βŸΆπ‘ˆ ∧ βˆ€π‘£ ∈ 𝑉 𝑣 βŠ† (π‘”β€˜π‘£)) β†’ βˆƒπ‘“((Fun 𝑓 ∧ dom 𝑓 βŠ† π‘ˆ ∧ ran 𝑓 βŠ† 𝐽) ∧ (ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))))
243242exlimdv 1934 . 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 394   ∧ w3a 1085   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βˆͺ cuni 4907  βˆͺ ciun 4996   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€“ontoβ†’wfo 6540  β€˜cfv 6542   β‰Ό cdom 8939  Fincfn 8941  Topctop 22615  Refcref 23226  LocFinclocfin 23228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-reg 9589  ax-inf2 9638  ax-ac2 10460
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-r1 9761  df-rank 9762  df-card 9936  df-ac 10113  df-top 22616  df-ref 23229  df-locfin 23231
This theorem is referenced by:  locfinref  33119
  Copyright terms: Public domain W3C validator