MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  restmetu Structured version   Visualization version   GIF version
Theorem restmetu 24071
Description: The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.)
Assertion
Ref Expression
restmetu ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))))
Proof of Theorem restmetu
Dummy variables π‘Ž 𝑏 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1137 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 β‰  βˆ…)
2 psmetres2 23812 . . . . 5 ((𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄))
323adant1 1131 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄))
4 oveq2 7414 . . . . . . . 8 (π‘Ž = 𝑏 β†’ (0[,)π‘Ž) = (0[,)𝑏))
54imaeq2d 6058 . . . . . . 7 (π‘Ž = 𝑏 β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
65cbvmptv 5261 . . . . . 6 (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) = (𝑏 ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
76rneqi 5935 . . . . 5 ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) = ran (𝑏 ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
87metustfbas 24058 . . . 4 ((𝐴 β‰  βˆ… ∧ (𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄)) β†’ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∈ (fBasβ€˜(𝐴 Γ— 𝐴)))
91, 3, 8syl2anc 585 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∈ (fBasβ€˜(𝐴 Γ— 𝐴)))
10 fgval 23366 . . 3 (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∈ (fBasβ€˜(𝐴 Γ— 𝐴)) β†’ ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
119, 10syl 17 . 2 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
12 metuval 24050 . . 3 ((𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄) β†’ (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))) = ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))))
133, 12syl 17 . 2 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))) = ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))))
14 fvex 6902 . . . 4 (metUnifβ€˜π·) ∈ V
153elfvexd 6928 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 ∈ V)
1615, 15xpexd 7735 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) ∈ V)
17 restval 17369 . . . 4 (((metUnifβ€˜π·) ∈ V ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))))
1814, 16, 17sylancr 588 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))))
19 inss2 4229 . . . . . . . . . . 11 (𝑣 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
20 sseq1 4007 . . . . . . . . . . 11 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ (𝑒 βŠ† (𝐴 Γ— 𝐴) ↔ (𝑣 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)))
2119, 20mpbiri 258 . . . . . . . . . 10 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝑒 βŠ† (𝐴 Γ— 𝐴))
22 vex 3479 . . . . . . . . . . 11 𝑒 ∈ V
2322elpw 4606 . . . . . . . . . 10 (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ↔ 𝑒 βŠ† (𝐴 Γ— 𝐴))
2421, 23sylibr 233 . . . . . . . . 9 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
2524rexlimivw 3152 . . . . . . . 8 (βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
2625adantl 483 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
27 nfv 1918 . . . . . . . . . . . 12 β„²π‘Ž(((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
28 nfmpt1 5256 . . . . . . . . . . . . . 14 β„²π‘Ž(π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
2928nfrn 5950 . . . . . . . . . . . . 13 β„²π‘Žran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
3029nfcri 2891 . . . . . . . . . . . 12 β„²π‘Ž 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
3127, 30nfan 1903 . . . . . . . . . . 11 β„²π‘Ž((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))))
32 nfv 1918 . . . . . . . . . . 11 β„²π‘Ž 𝑀 βŠ† 𝑣
3331, 32nfan 1903 . . . . . . . . . 10 β„²π‘Ž(((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣)
34 nfmpt1 5256 . . . . . . . . . . . . 13 β„²π‘Ž(π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
3534nfrn 5950 . . . . . . . . . . . 12 β„²π‘Žran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
36 nfcv 2904 . . . . . . . . . . . 12 β„²π‘Žπ’« 𝑒
3735, 36nfin 4216 . . . . . . . . . . 11 β„²π‘Ž(ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒)
38 nfcv 2904 . . . . . . . . . . 11 β„²π‘Žβˆ…
3937, 38nfne 3044 . . . . . . . . . 10 β„²π‘Ž(ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…
40 simplr 768 . . . . . . . . . . . . 13 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ π‘Ž ∈ ℝ+)
41 ineq1 4205 . . . . . . . . . . . . . . 15 (𝑀 = (◑𝐷 β€œ (0[,)π‘Ž)) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4241adantl 483 . . . . . . . . . . . . . 14 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
43 simp2 1138 . . . . . . . . . . . . . . . 16 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐷 ∈ (PsMetβ€˜π‘‹))
44 psmetf 23804 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (PsMetβ€˜π‘‹) β†’ 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„*)
45 ffun 6718 . . . . . . . . . . . . . . . 16 (𝐷:(𝑋 Γ— 𝑋)βŸΆβ„* β†’ Fun 𝐷)
46 respreima 7065 . . . . . . . . . . . . . . . 16 (Fun 𝐷 β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4743, 44, 45, 464syl 19 . . . . . . . . . . . . . . 15 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4847ad6antr 735 . . . . . . . . . . . . . 14 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4942, 48eqtr4d 2776 . . . . . . . . . . . . 13 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
50 rspe 3247 . . . . . . . . . . . . 13 ((π‘Ž ∈ ℝ+ ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) β†’ βˆƒπ‘Ž ∈ ℝ+ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
5140, 49, 50syl2anc 585 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ βˆƒπ‘Ž ∈ ℝ+ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
52 vex 3479 . . . . . . . . . . . . . 14 𝑀 ∈ V
5352inex1 5317 . . . . . . . . . . . . 13 (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ V
54 eqid 2733 . . . . . . . . . . . . . 14 (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) = (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
5554elrnmpt 5954 . . . . . . . . . . . . 13 ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ V β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))))
5653, 55ax-mp 5 . . . . . . . . . . . 12 ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
5751, 56sylibr 233 . . . . . . . . . . 11 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))))
58 simpllr 775 . . . . . . . . . . . . 13 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ 𝑀 βŠ† 𝑣)
59 ssinss1 4237 . . . . . . . . . . . . 13 (𝑀 βŠ† 𝑣 β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣)
6058, 59syl 17 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣)
61 inss2 4229 . . . . . . . . . . . . 13 (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
6261a1i 11 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴))
63 pweq 4616 . . . . . . . . . . . . . . . 16 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝒫 𝑒 = 𝒫 (𝑣 ∩ (𝐴 Γ— 𝐴)))
6463eleq2d 2820 . . . . . . . . . . . . . . 15 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 Γ— 𝐴))))
6553elpw 4606 . . . . . . . . . . . . . . 15 ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 Γ— 𝐴)) ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑣 ∩ (𝐴 Γ— 𝐴)))
6664, 65bitrdi 287 . . . . . . . . . . . . . 14 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑣 ∩ (𝐴 Γ— 𝐴))))
67 ssin 4230 . . . . . . . . . . . . . 14 (((𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣 ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)) ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑣 ∩ (𝐴 Γ— 𝐴)))
6866, 67bitr4di 289 . . . . . . . . . . . . 13 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ ((𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣 ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴))))
6968ad5antlr 734 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ ((𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣 ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴))))
7060, 62, 69mpbir2and 712 . . . . . . . . . . 11 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒)
71 inelcm 4464 . . . . . . . . . . 11 (((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
7257, 70, 71syl2anc 585 . . . . . . . . . 10 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
73 simplr 768 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) β†’ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))))
74 eqid 2733 . . . . . . . . . . . . 13 (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) = (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
7574elrnmpt 5954 . . . . . . . . . . . 12 (𝑀 ∈ V β†’ (𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))))
7675elv 3481 . . . . . . . . . . 11 (𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž)))
7773, 76sylib 217 . . . . . . . . . 10 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) β†’ βˆƒπ‘Ž ∈ ℝ+ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž)))
7833, 39, 72, 77r19.29af2 3265 . . . . . . . . 9 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
79 ssn0 4400 . . . . . . . . . . . . . 14 ((𝐴 βŠ† 𝑋 ∧ 𝐴 β‰  βˆ…) β†’ 𝑋 β‰  βˆ…)
8079ancoms 460 . . . . . . . . . . . . 13 ((𝐴 β‰  βˆ… ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 β‰  βˆ…)
81803adant2 1132 . . . . . . . . . . . 12 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 β‰  βˆ…)
82 metuel 24065 . . . . . . . . . . . 12 ((𝑋 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹)) β†’ (𝑣 ∈ (metUnifβ€˜π·) ↔ (𝑣 βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)))
8381, 43, 82syl2anc 585 . . . . . . . . . . 11 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑣 ∈ (metUnifβ€˜π·) ↔ (𝑣 βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)))
8483simplbda 501 . . . . . . . . . 10 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)
8584adantr 482 . . . . . . . . 9 ((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)
8678, 85r19.29a 3163 . . . . . . . 8 ((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
8786r19.29an 3159 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
8826, 87jca 513 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…))
89 simprl 770 . . . . . . . . . . 11 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
9089elpwid 4611 . . . . . . . . . 10 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 βŠ† (𝐴 Γ— 𝐴))
91 simpl3 1194 . . . . . . . . . . 11 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝐴 βŠ† 𝑋)
92 xpss12 5691 . . . . . . . . . . 11 ((𝐴 βŠ† 𝑋 ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
9391, 91, 92syl2anc 585 . . . . . . . . . 10 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
9490, 93sstrd 3992 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 βŠ† (𝑋 Γ— 𝑋))
95 difssd 4132 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) βŠ† (𝑋 Γ— 𝑋))
9694, 95unssd 4186 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† (𝑋 Γ— 𝑋))
97 simplr 768 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑏 ∈ ℝ+)
98 eqidd 2734 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)𝑏)))
994imaeq2d 6058 . . . . . . . . . . . . 13 (π‘Ž = 𝑏 β†’ (◑𝐷 β€œ (0[,)π‘Ž)) = (◑𝐷 β€œ (0[,)𝑏)))
10099rspceeqv 3633 . . . . . . . . . . . 12 ((𝑏 ∈ ℝ+ ∧ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)𝑏))) β†’ βˆƒπ‘Ž ∈ ℝ+ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)π‘Ž)))
10197, 98, 100syl2anc 585 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ βˆƒπ‘Ž ∈ ℝ+ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)π‘Ž)))
10243ad4antr 731 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝐷 ∈ (PsMetβ€˜π‘‹))
103 cnvexg 7912 . . . . . . . . . . . 12 (𝐷 ∈ (PsMetβ€˜π‘‹) β†’ ◑𝐷 ∈ V)
104 imaexg 7903 . . . . . . . . . . . 12 (◑𝐷 ∈ V β†’ (◑𝐷 β€œ (0[,)𝑏)) ∈ V)
10574elrnmpt 5954 . . . . . . . . . . . 12 ((◑𝐷 β€œ (0[,)𝑏)) ∈ V β†’ ((◑𝐷 β€œ (0[,)𝑏)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)π‘Ž))))
106102, 103, 104, 1054syl 19 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)π‘Ž))))
107101, 106mpbird 257 . . . . . . . . . 10 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))))
108 cnvimass 6078 . . . . . . . . . . . . . . . 16 (◑𝐷 β€œ (0[,)𝑏)) βŠ† dom 𝐷
109108, 44fssdm 6735 . . . . . . . . . . . . . . 15 (𝐷 ∈ (PsMetβ€˜π‘‹) β†’ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑋 Γ— 𝑋))
110102, 109syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑋 Γ— 𝑋))
111 ssdif0 4363 . . . . . . . . . . . . . 14 ((◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑋 Γ— 𝑋) ↔ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) = βˆ…)
112110, 111sylib 217 . . . . . . . . . . . . 13 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) = βˆ…)
113 0ss 4396 . . . . . . . . . . . . 13 βˆ… βŠ† 𝑒
114112, 113eqsstrdi 4036 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βŠ† 𝑒)
115 respreima 7065 . . . . . . . . . . . . . 14 (Fun 𝐷 β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) = ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)))
116102, 44, 45, 1154syl 19 . . . . . . . . . . . . 13 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) = ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)))
117 simpr 486 . . . . . . . . . . . . . 14 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
118 simpllr 775 . . . . . . . . . . . . . . 15 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑣 ∈ 𝒫 𝑒)
119118elpwid 4611 . . . . . . . . . . . . . 14 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑣 βŠ† 𝑒)
120117, 119eqsstrrd 4021 . . . . . . . . . . . . 13 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) βŠ† 𝑒)
121116, 120eqsstrrd 4021 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑒)
122114, 121unssd 4186 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
123 ssundif 4487 . . . . . . . . . . . 12 ((◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ↔ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– 𝑒) βŠ† ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)))
124 difcom 4488 . . . . . . . . . . . 12 (((◑𝐷 β€œ (0[,)𝑏)) βˆ– 𝑒) βŠ† ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ↔ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† 𝑒)
125 difdif2 4286 . . . . . . . . . . . . 13 ((◑𝐷 β€œ (0[,)𝑏)) βˆ– ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) = (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)))
126125sseq1i 4010 . . . . . . . . . . . 12 (((◑𝐷 β€œ (0[,)𝑏)) βˆ– ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† 𝑒 ↔ (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
127123, 124, 1263bitri 297 . . . . . . . . . . 11 ((◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ↔ (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
128122, 127sylibr 233 . . . . . . . . . 10 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
129 sseq1 4007 . . . . . . . . . . 11 (𝑀 = (◑𝐷 β€œ (0[,)𝑏)) β†’ (𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ↔ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)))))
130129rspcev 3613 . . . . . . . . . 10 (((◑𝐷 β€œ (0[,)𝑏)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ∧ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)))) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
131107, 128, 130syl2anc 585 . . . . . . . . 9 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
132 elin 3964 . . . . . . . . . . . . . 14 (𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) ↔ (𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∧ 𝑣 ∈ 𝒫 𝑒))
1336elrnmpt 5954 . . . . . . . . . . . . . . . 16 (𝑣 ∈ V β†’ (𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
134133elv 3481 . . . . . . . . . . . . . . 15 (𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
135134anbi1i 625 . . . . . . . . . . . . . 14 ((𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∧ 𝑣 ∈ 𝒫 𝑒) ↔ (βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑒))
136 ancom 462 . . . . . . . . . . . . . 14 ((βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑒) ↔ (𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
137132, 135, 1363bitri 297 . . . . . . . . . . . . 13 (𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) ↔ (𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
138137exbii 1851 . . . . . . . . . . . 12 (βˆƒπ‘£ 𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) ↔ βˆƒπ‘£(𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
139 n0 4346 . . . . . . . . . . . 12 ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒))
140 df-rex 3072 . . . . . . . . . . . 12 (βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) ↔ βˆƒπ‘£(𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
141138, 139, 1403bitr4i 303 . . . . . . . . . . 11 ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ… ↔ βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
142141biimpi 215 . . . . . . . . . 10 ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ… β†’ βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
143142ad2antll 728 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
144131, 143r19.29vva 3214 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
14581adantr 482 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑋 β‰  βˆ…)
14643adantr 482 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝐷 ∈ (PsMetβ€˜π‘‹))
147 metuel 24065 . . . . . . . . 9 ((𝑋 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹)) β†’ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·) ↔ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))))
148145, 146, 147syl2anc 585 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·) ↔ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))))
14996, 144, 148mpbir2and 712 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·))
150 indir 4275 . . . . . . . . 9 ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ (((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ∩ (𝐴 Γ— 𝐴)))
151 disjdifr 4472 . . . . . . . . . 10 (((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ∩ (𝐴 Γ— 𝐴)) = βˆ…
152151uneq2i 4160 . . . . . . . . 9 ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ (((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ∩ (𝐴 Γ— 𝐴))) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ βˆ…)
153 un0 4390 . . . . . . . . 9 ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ βˆ…) = (𝑒 ∩ (𝐴 Γ— 𝐴))
154150, 152, 1533eqtri 2765 . . . . . . . 8 ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)) = (𝑒 ∩ (𝐴 Γ— 𝐴))
155 df-ss 3965 . . . . . . . . 9 (𝑒 βŠ† (𝐴 Γ— 𝐴) ↔ (𝑒 ∩ (𝐴 Γ— 𝐴)) = 𝑒)
15690, 155sylib 217 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝑒 ∩ (𝐴 Γ— 𝐴)) = 𝑒)
157154, 156eqtr2id 2786 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 = ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)))
158 ineq1 4205 . . . . . . . 8 (𝑣 = (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) β†’ (𝑣 ∩ (𝐴 Γ— 𝐴)) = ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)))
159158rspceeqv 3633 . . . . . . 7 (((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·) ∧ 𝑒 = ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
160149, 157, 159syl2anc 585 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
16188, 160impbida 800 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) ↔ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)))
162 eqid 2733 . . . . . . 7 (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) = (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴)))
163162elrnmpt 5954 . . . . . 6 (𝑒 ∈ V β†’ (𝑒 ∈ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) ↔ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))))
164163elv 3481 . . . . 5 (𝑒 ∈ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) ↔ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
165 pweq 4616 . . . . . . . 8 (𝑣 = 𝑒 β†’ 𝒫 𝑣 = 𝒫 𝑒)
166165ineq2d 4212 . . . . . . 7 (𝑣 = 𝑒 β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) = (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒))
167166neeq1d 3001 . . . . . 6 (𝑣 = 𝑒 β†’ ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ… ↔ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…))
168167elrab 3683 . . . . 5 (𝑒 ∈ {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…} ↔ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…))
169161, 164, 1683bitr4g 314 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑒 ∈ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) ↔ 𝑒 ∈ {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…}))
170169eqrdv 2731 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
17118, 170eqtrd 2773 . 2 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
17211, 13, 1713eqtr4rd 2784 1 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679  Fun wfun 6535  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406  0cc0 11107  β„*cxr 11244  β„+crp 12971  [,)cico 13323   β†Ύt crest 17363  PsMetcpsmet 20921  fBascfbas 20925  filGencfg 20926  metUnifcmetu 20928
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
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-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-rp 12972  df-ico 13327  df-rest 17365  df-psmet 20929  df-fbas 20934  df-fg 20935  df-metu 20936
This theorem is referenced by:  reust  24890  qqhucn  32961
  Copyright terms: Public domain W3C validator