MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  restmetu Structured version   Visualization version   GIF version
Theorem restmetu 24389
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 1133 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 β‰  βˆ…)
2 psmetres2 24130 . . . . 5 ((𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄))
323adant1 1127 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄))
4 oveq2 7409 . . . . . . . 8 (π‘Ž = 𝑏 β†’ (0[,)π‘Ž) = (0[,)𝑏))
54imaeq2d 6049 . . . . . . 7 (π‘Ž = 𝑏 β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
65cbvmptv 5251 . . . . . 6 (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) = (𝑏 ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
76rneqi 5926 . . . . 5 ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) = ran (𝑏 ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
87metustfbas 24376 . . . 4 ((𝐴 β‰  βˆ… ∧ (𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄)) β†’ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∈ (fBasβ€˜(𝐴 Γ— 𝐴)))
91, 3, 8syl2anc 583 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∈ (fBasβ€˜(𝐴 Γ— 𝐴)))
10 fgval 23684 . . 3 (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∈ (fBasβ€˜(𝐴 Γ— 𝐴)) β†’ ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
119, 10syl 17 . 2 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
12 metuval 24368 . . 3 ((𝐷 β†Ύ (𝐴 Γ— 𝐴)) ∈ (PsMetβ€˜π΄) β†’ (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))) = ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))))
133, 12syl 17 . 2 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))) = ((𝐴 Γ— 𝐴)filGenran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))))
14 fvex 6894 . . . 4 (metUnifβ€˜π·) ∈ V
153elfvexd 6920 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 ∈ V)
1615, 15xpexd 7731 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) ∈ V)
17 restval 17368 . . . 4 (((metUnifβ€˜π·) ∈ V ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))))
1814, 16, 17sylancr 586 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))))
19 inss2 4221 . . . . . . . . . . 11 (𝑣 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
20 sseq1 3999 . . . . . . . . . . 11 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ (𝑒 βŠ† (𝐴 Γ— 𝐴) ↔ (𝑣 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)))
2119, 20mpbiri 258 . . . . . . . . . 10 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝑒 βŠ† (𝐴 Γ— 𝐴))
22 vex 3470 . . . . . . . . . . 11 𝑒 ∈ V
2322elpw 4598 . . . . . . . . . 10 (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ↔ 𝑒 βŠ† (𝐴 Γ— 𝐴))
2421, 23sylibr 233 . . . . . . . . 9 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
2524rexlimivw 3143 . . . . . . . 8 (βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
2625adantl 481 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
27 nfv 1909 . . . . . . . . . . . 12 β„²π‘Ž(((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
28 nfmpt1 5246 . . . . . . . . . . . . . 14 β„²π‘Ž(π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
2928nfrn 5941 . . . . . . . . . . . . 13 β„²π‘Žran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
3029nfcri 2882 . . . . . . . . . . . 12 β„²π‘Ž 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
3127, 30nfan 1894 . . . . . . . . . . 11 β„²π‘Ž((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))))
32 nfv 1909 . . . . . . . . . . 11 β„²π‘Ž 𝑀 βŠ† 𝑣
3331, 32nfan 1894 . . . . . . . . . 10 β„²π‘Ž(((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣)
34 nfmpt1 5246 . . . . . . . . . . . . 13 β„²π‘Ž(π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
3534nfrn 5941 . . . . . . . . . . . 12 β„²π‘Žran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
36 nfcv 2895 . . . . . . . . . . . 12 β„²π‘Žπ’« 𝑒
3735, 36nfin 4208 . . . . . . . . . . 11 β„²π‘Ž(ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒)
38 nfcv 2895 . . . . . . . . . . 11 β„²π‘Žβˆ…
3937, 38nfne 3035 . . . . . . . . . 10 β„²π‘Ž(ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…
40 simplr 766 . . . . . . . . . . . . 13 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ π‘Ž ∈ ℝ+)
41 ineq1 4197 . . . . . . . . . . . . . . 15 (𝑀 = (◑𝐷 β€œ (0[,)π‘Ž)) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4241adantl 481 . . . . . . . . . . . . . 14 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
43 simp2 1134 . . . . . . . . . . . . . . . 16 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐷 ∈ (PsMetβ€˜π‘‹))
44 psmetf 24122 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (PsMetβ€˜π‘‹) β†’ 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„*)
45 ffun 6710 . . . . . . . . . . . . . . . 16 (𝐷:(𝑋 Γ— 𝑋)βŸΆβ„* β†’ Fun 𝐷)
46 respreima 7057 . . . . . . . . . . . . . . . 16 (Fun 𝐷 β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4743, 44, 45, 464syl 19 . . . . . . . . . . . . . . 15 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4847ad6antr 733 . . . . . . . . . . . . . 14 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)) = ((◑𝐷 β€œ (0[,)π‘Ž)) ∩ (𝐴 Γ— 𝐴)))
4942, 48eqtr4d 2767 . . . . . . . . . . . . 13 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
50 rspe 3238 . . . . . . . . . . . . 13 ((π‘Ž ∈ ℝ+ ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) β†’ βˆƒπ‘Ž ∈ ℝ+ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
5140, 49, 50syl2anc 583 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ βˆƒπ‘Ž ∈ ℝ+ (𝑀 ∩ (𝐴 Γ— 𝐴)) = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
52 vex 3470 . . . . . . . . . . . . . 14 𝑀 ∈ V
5352inex1 5307 . . . . . . . . . . . . 13 (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ V
54 eqid 2724 . . . . . . . . . . . . . 14 (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) = (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž)))
5554elrnmpt 5945 . . . . . . . . . . . . 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 773 . . . . . . . . . . . . 13 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ 𝑀 βŠ† 𝑣)
59 ssinss1 4229 . . . . . . . . . . . . 13 (𝑀 βŠ† 𝑣 β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣)
6058, 59syl 17 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣)
61 inss2 4221 . . . . . . . . . . . . 13 (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
6261a1i 11 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴))
63 pweq 4608 . . . . . . . . . . . . . . . 16 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ 𝒫 𝑒 = 𝒫 (𝑣 ∩ (𝐴 Γ— 𝐴)))
6463eleq2d 2811 . . . . . . . . . . . . . . 15 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 Γ— 𝐴))))
6553elpw 4598 . . . . . . . . . . . . . . 15 ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 Γ— 𝐴)) ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑣 ∩ (𝐴 Γ— 𝐴)))
6664, 65bitrdi 287 . . . . . . . . . . . . . 14 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑣 ∩ (𝐴 Γ— 𝐴))))
67 ssin 4222 . . . . . . . . . . . . . 14 (((𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣 ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)) ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑣 ∩ (𝐴 Γ— 𝐴)))
6866, 67bitr4di 289 . . . . . . . . . . . . 13 (𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ ((𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣 ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴))))
6968ad5antlr 732 . . . . . . . . . . . 12 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒 ↔ ((𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑣 ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴))))
7060, 62, 69mpbir2and 710 . . . . . . . . . . 11 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒)
71 inelcm 4456 . . . . . . . . . . 11 (((𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∧ (𝑀 ∩ (𝐴 Γ— 𝐴)) ∈ 𝒫 𝑒) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
7257, 70, 71syl2anc 583 . . . . . . . . . 10 ((((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) ∧ π‘Ž ∈ ℝ+) ∧ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
73 simplr 766 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) β†’ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))))
74 eqid 2724 . . . . . . . . . . . . 13 (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) = (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))
7574elrnmpt 5945 . . . . . . . . . . . 12 (𝑀 ∈ V β†’ (𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž))))
7675elv 3472 . . . . . . . . . . 11 (𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘Ž ∈ ℝ+ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž)))
7773, 76sylib 217 . . . . . . . . . 10 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) β†’ βˆƒπ‘Ž ∈ ℝ+ 𝑀 = (◑𝐷 β€œ (0[,)π‘Ž)))
7833, 39, 72, 77r19.29af2 3256 . . . . . . . . 9 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))) ∧ 𝑀 βŠ† 𝑣) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
79 ssn0 4392 . . . . . . . . . . . . . 14 ((𝐴 βŠ† 𝑋 ∧ 𝐴 β‰  βˆ…) β†’ 𝑋 β‰  βˆ…)
8079ancoms 458 . . . . . . . . . . . . 13 ((𝐴 β‰  βˆ… ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 β‰  βˆ…)
81803adant2 1128 . . . . . . . . . . . 12 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 β‰  βˆ…)
82 metuel 24383 . . . . . . . . . . . 12 ((𝑋 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹)) β†’ (𝑣 ∈ (metUnifβ€˜π·) ↔ (𝑣 βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)))
8381, 43, 82syl2anc 583 . . . . . . . . . . 11 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑣 ∈ (metUnifβ€˜π·) ↔ (𝑣 βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)))
8483simplbda 499 . . . . . . . . . 10 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)
8584adantr 480 . . . . . . . . 9 ((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† 𝑣)
8678, 85r19.29a 3154 . . . . . . . 8 ((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (metUnifβ€˜π·)) ∧ 𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
8786r19.29an 3150 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)
8826, 87jca 511 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…))
89 simprl 768 . . . . . . . . . . 11 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴))
9089elpwid 4603 . . . . . . . . . 10 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 βŠ† (𝐴 Γ— 𝐴))
91 simpl3 1190 . . . . . . . . . . 11 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝐴 βŠ† 𝑋)
92 xpss12 5681 . . . . . . . . . . 11 ((𝐴 βŠ† 𝑋 ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
9391, 91, 92syl2anc 583 . . . . . . . . . 10 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
9490, 93sstrd 3984 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 βŠ† (𝑋 Γ— 𝑋))
95 difssd 4124 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) βŠ† (𝑋 Γ— 𝑋))
9694, 95unssd 4178 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† (𝑋 Γ— 𝑋))
97 simplr 766 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑏 ∈ ℝ+)
98 eqidd 2725 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)𝑏)))
994imaeq2d 6049 . . . . . . . . . . . . 13 (π‘Ž = 𝑏 β†’ (◑𝐷 β€œ (0[,)π‘Ž)) = (◑𝐷 β€œ (0[,)𝑏)))
10099rspceeqv 3625 . . . . . . . . . . . 12 ((𝑏 ∈ ℝ+ ∧ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)𝑏))) β†’ βˆƒπ‘Ž ∈ ℝ+ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)π‘Ž)))
10197, 98, 100syl2anc 583 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ βˆƒπ‘Ž ∈ ℝ+ (◑𝐷 β€œ (0[,)𝑏)) = (◑𝐷 β€œ (0[,)π‘Ž)))
10243ad4antr 729 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝐷 ∈ (PsMetβ€˜π‘‹))
103 cnvexg 7908 . . . . . . . . . . . 12 (𝐷 ∈ (PsMetβ€˜π‘‹) β†’ ◑𝐷 ∈ V)
104 imaexg 7899 . . . . . . . . . . . 12 (◑𝐷 ∈ V β†’ (◑𝐷 β€œ (0[,)𝑏)) ∈ V)
10574elrnmpt 5945 . . . . . . . . . . . 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 6070 . . . . . . . . . . . . . . . 16 (◑𝐷 β€œ (0[,)𝑏)) βŠ† dom 𝐷
109108, 44fssdm 6727 . . . . . . . . . . . . . . 15 (𝐷 ∈ (PsMetβ€˜π‘‹) β†’ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑋 Γ— 𝑋))
110102, 109syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑋 Γ— 𝑋))
111 ssdif0 4355 . . . . . . . . . . . . . 14 ((◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑋 Γ— 𝑋) ↔ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) = βˆ…)
112110, 111sylib 217 . . . . . . . . . . . . 13 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) = βˆ…)
113 0ss 4388 . . . . . . . . . . . . 13 βˆ… βŠ† 𝑒
114112, 113eqsstrdi 4028 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βŠ† 𝑒)
115 respreima 7057 . . . . . . . . . . . . . 14 (Fun 𝐷 β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) = ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)))
116102, 44, 45, 1154syl 19 . . . . . . . . . . . . 13 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) = ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)))
117 simpr 484 . . . . . . . . . . . . . 14 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
118 simpllr 773 . . . . . . . . . . . . . . 15 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑣 ∈ 𝒫 𝑒)
119118elpwid 4603 . . . . . . . . . . . . . 14 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ 𝑣 βŠ† 𝑒)
120117, 119eqsstrrd 4013 . . . . . . . . . . . . 13 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) βŠ† 𝑒)
121116, 120eqsstrrd 4013 . . . . . . . . . . . 12 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑒)
122114, 121unssd 4178 . . . . . . . . . . 11 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
123 ssundif 4479 . . . . . . . . . . . 12 ((◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ↔ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– 𝑒) βŠ† ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)))
124 difcom 4480 . . . . . . . . . . . 12 (((◑𝐷 β€œ (0[,)𝑏)) βˆ– 𝑒) βŠ† ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ↔ ((◑𝐷 β€œ (0[,)𝑏)) βˆ– ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† 𝑒)
125 difdif2 4278 . . . . . . . . . . . . 13 ((◑𝐷 β€œ (0[,)𝑏)) βˆ– ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) = (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴)))
126125sseq1i 4002 . . . . . . . . . . . 12 (((◑𝐷 β€œ (0[,)𝑏)) βˆ– ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† 𝑒 ↔ (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
127123, 124, 1263bitri 297 . . . . . . . . . . 11 ((◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ↔ (((◑𝐷 β€œ (0[,)𝑏)) βˆ– (𝑋 Γ— 𝑋)) βˆͺ ((◑𝐷 β€œ (0[,)𝑏)) ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
128122, 127sylibr 233 . . . . . . . . . 10 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
129 sseq1 3999 . . . . . . . . . . 11 (𝑀 = (◑𝐷 β€œ (0[,)𝑏)) β†’ (𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ↔ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)))))
130129rspcev 3604 . . . . . . . . . 10 (((◑𝐷 β€œ (0[,)𝑏)) ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž))) ∧ (◑𝐷 β€œ (0[,)𝑏)) βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)))) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
131107, 128, 130syl2anc 583 . . . . . . . . 9 ((((((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) ∧ 𝑣 ∈ 𝒫 𝑒) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
132 elin 3956 . . . . . . . . . . . . . 14 (𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) ↔ (𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∧ 𝑣 ∈ 𝒫 𝑒))
1336elrnmpt 5945 . . . . . . . . . . . . . . . 16 (𝑣 ∈ V β†’ (𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
134133elv 3472 . . . . . . . . . . . . . . 15 (𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ↔ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
135134anbi1i 623 . . . . . . . . . . . . . 14 ((𝑣 ∈ ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∧ 𝑣 ∈ 𝒫 𝑒) ↔ (βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑒))
136 ancom 460 . . . . . . . . . . . . . 14 ((βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑒) ↔ (𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
137132, 135, 1363bitri 297 . . . . . . . . . . . . 13 (𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) ↔ (𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
138137exbii 1842 . . . . . . . . . . . 12 (βˆƒπ‘£ 𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) ↔ βˆƒπ‘£(𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
139 n0 4338 . . . . . . . . . . . 12 ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒))
140 df-rex 3063 . . . . . . . . . . . 12 (βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)) ↔ βˆƒπ‘£(𝑣 ∈ 𝒫 𝑒 ∧ βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏))))
141138, 139, 1403bitr4i 303 . . . . . . . . . . 11 ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ… ↔ βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
142141biimpi 215 . . . . . . . . . 10 ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ… β†’ βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
143142ad2antll 726 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ βˆƒπ‘£ ∈ 𝒫 π‘’βˆƒπ‘ ∈ ℝ+ 𝑣 = (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)𝑏)))
144131, 143r19.29vva 3205 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))
14581adantr 480 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑋 β‰  βˆ…)
14643adantr 480 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝐷 ∈ (PsMetβ€˜π‘‹))
147 metuel 24383 . . . . . . . . 9 ((𝑋 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹)) β†’ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·) ↔ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))))
148145, 146, 147syl2anc 583 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·) ↔ ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) βŠ† (𝑋 Γ— 𝑋) ∧ βˆƒπ‘€ ∈ ran (π‘Ž ∈ ℝ+ ↦ (◑𝐷 β€œ (0[,)π‘Ž)))𝑀 βŠ† (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))))))
14996, 144, 148mpbir2and 710 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·))
150 indir 4267 . . . . . . . . 9 ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ (((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ∩ (𝐴 Γ— 𝐴)))
151 disjdifr 4464 . . . . . . . . . 10 (((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ∩ (𝐴 Γ— 𝐴)) = βˆ…
152151uneq2i 4152 . . . . . . . . 9 ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ (((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴)) ∩ (𝐴 Γ— 𝐴))) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ βˆ…)
153 un0 4382 . . . . . . . . 9 ((𝑒 ∩ (𝐴 Γ— 𝐴)) βˆͺ βˆ…) = (𝑒 ∩ (𝐴 Γ— 𝐴))
154150, 152, 1533eqtri 2756 . . . . . . . 8 ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)) = (𝑒 ∩ (𝐴 Γ— 𝐴))
155 df-ss 3957 . . . . . . . . 9 (𝑒 βŠ† (𝐴 Γ— 𝐴) ↔ (𝑒 ∩ (𝐴 Γ— 𝐴)) = 𝑒)
15690, 155sylib 217 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ (𝑒 ∩ (𝐴 Γ— 𝐴)) = 𝑒)
157154, 156eqtr2id 2777 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ 𝑒 = ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)))
158 ineq1 4197 . . . . . . . 8 (𝑣 = (𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) β†’ (𝑣 ∩ (𝐴 Γ— 𝐴)) = ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴)))
159158rspceeqv 3625 . . . . . . 7 (((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∈ (metUnifβ€˜π·) ∧ 𝑒 = ((𝑒 βˆͺ ((𝑋 Γ— 𝑋) βˆ– (𝐴 Γ— 𝐴))) ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
160149, 157, 159syl2anc 583 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)) β†’ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
16188, 160impbida 798 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)) ↔ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…)))
162 eqid 2724 . . . . . . 7 (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) = (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴)))
163162elrnmpt 5945 . . . . . 6 (𝑒 ∈ V β†’ (𝑒 ∈ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) ↔ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴))))
164163elv 3472 . . . . 5 (𝑒 ∈ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) ↔ βˆƒπ‘£ ∈ (metUnifβ€˜π·)𝑒 = (𝑣 ∩ (𝐴 Γ— 𝐴)))
165 pweq 4608 . . . . . . . 8 (𝑣 = 𝑒 β†’ 𝒫 𝑣 = 𝒫 𝑒)
166165ineq2d 4204 . . . . . . 7 (𝑣 = 𝑒 β†’ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) = (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒))
167166neeq1d 2992 . . . . . 6 (𝑣 = 𝑒 β†’ ((ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ… ↔ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…))
168167elrab 3675 . . . . 5 (𝑒 ∈ {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…} ↔ (𝑒 ∈ 𝒫 (𝐴 Γ— 𝐴) ∧ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑒) β‰  βˆ…))
169161, 164, 1683bitr4g 314 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑒 ∈ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) ↔ 𝑒 ∈ {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…}))
170169eqrdv 2722 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ran (𝑣 ∈ (metUnifβ€˜π·) ↦ (𝑣 ∩ (𝐴 Γ— 𝐴))) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
17118, 170eqtrd 2764 . 2 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = {𝑣 ∈ 𝒫 (𝐴 Γ— 𝐴) ∣ (ran (π‘Ž ∈ ℝ+ ↦ (β—‘(𝐷 β†Ύ (𝐴 Γ— 𝐴)) β€œ (0[,)π‘Ž))) ∩ 𝒫 𝑣) β‰  βˆ…})
17211, 13, 1713eqtr4rd 2775 1 ((𝐴 β‰  βˆ… ∧ 𝐷 ∈ (PsMetβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((metUnifβ€˜π·) β†Ύt (𝐴 Γ— 𝐴)) = (metUnifβ€˜(𝐷 β†Ύ (𝐴 Γ— 𝐴))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2932  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  π’« cpw 4594   ↦ cmpt 5221   Γ— cxp 5664  β—‘ccnv 5665  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669  Fun wfun 6527  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  0cc0 11105  β„*cxr 11243  β„+crp 12970  [,)cico 13322   β†Ύt crest 17362  PsMetcpsmet 21207  fBascfbas 21211  filGencfg 21212  metUnifcmetu 21214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-so 5579  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-er 8698  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-rp 12971  df-ico 13326  df-rest 17364  df-psmet 21215  df-fbas 21220  df-fg 21221  df-metu 21222
This theorem is referenced by:  reust  25219  qqhucn  33427
  Copyright terms: Public domain W3C validator