MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  restmetu Structured version   Visualization version   GIF version

Theorem restmetu 22422
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 1081 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → 𝐴 ≠ ∅)
2 psmetres2 22166 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴))
323adant1 1099 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴))
4 oveq2 6698 . . . . . . . 8 (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
54imaeq2d 5501 . . . . . . 7 (𝑎 = 𝑏 → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
65cbvmptv 4783 . . . . . 6 (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
76rneqi 5384 . . . . 5 ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
87metustfbas 22409 . . . 4 ((𝐴 ≠ ∅ ∧ (𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴)) → ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∈ (fBas‘(𝐴 × 𝐴)))
91, 3, 8syl2anc 694 . . 3 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∈ (fBas‘(𝐴 × 𝐴)))
10 fgval 21721 . . 3 (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∈ (fBas‘(𝐴 × 𝐴)) → ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
119, 10syl 17 . 2 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
12 metuval 22401 . . 3 ((𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴) → (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))) = ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))))
133, 12syl 17 . 2 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))) = ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))))
14 fvex 6239 . . . 4 (metUnif‘𝐷) ∈ V
153elfvexd 6260 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → 𝐴 ∈ V)
16 xpexg 7002 . . . . 5 ((𝐴 ∈ V ∧ 𝐴 ∈ V) → (𝐴 × 𝐴) ∈ V)
1715, 15, 16syl2anc 694 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (𝐴 × 𝐴) ∈ V)
18 restval 16134 . . . 4 (((metUnif‘𝐷) ∈ V ∧ (𝐴 × 𝐴) ∈ V) → ((metUnif‘𝐷) ↾t (𝐴 × 𝐴)) = ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))))
1914, 17, 18sylancr 696 . . 3 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ((metUnif‘𝐷) ↾t (𝐴 × 𝐴)) = ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))))
20 inss2 3867 . . . . . . . . . . 11 (𝑣 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
21 sseq1 3659 . . . . . . . . . . 11 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → (𝑢 ⊆ (𝐴 × 𝐴) ↔ (𝑣 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)))
2220, 21mpbiri 248 . . . . . . . . . 10 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝑢 ⊆ (𝐴 × 𝐴))
23 vex 3234 . . . . . . . . . . 11 𝑢 ∈ V
2423elpw 4197 . . . . . . . . . 10 (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑢 ⊆ (𝐴 × 𝐴))
2522, 24sylibr 224 . . . . . . . . 9 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
2625rexlimivw 3058 . . . . . . . 8 (∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
2726adantl 481 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
28 nfv 1883 . . . . . . . . . . . 12 𝑎(((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
29 nfmpt1 4780 . . . . . . . . . . . . . 14 𝑎(𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
3029nfrn 5400 . . . . . . . . . . . . 13 𝑎ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
3130nfcri 2787 . . . . . . . . . . . 12 𝑎 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
3228, 31nfan 1868 . . . . . . . . . . 11 𝑎((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))))
33 nfv 1883 . . . . . . . . . . 11 𝑎 𝑤𝑣
3432, 33nfan 1868 . . . . . . . . . 10 𝑎(((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣)
35 nfmpt1 4780 . . . . . . . . . . . . 13 𝑎(𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
3635nfrn 5400 . . . . . . . . . . . 12 𝑎ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
37 nfcv 2793 . . . . . . . . . . . 12 𝑎𝒫 𝑢
3836, 37nfin 3853 . . . . . . . . . . 11 𝑎(ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢)
39 nfcv 2793 . . . . . . . . . . 11 𝑎
4038, 39nfne 2923 . . . . . . . . . 10 𝑎(ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅
41 simplr 807 . . . . . . . . . . . . 13 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
42 ineq1 3840 . . . . . . . . . . . . . . 15 (𝑤 = (𝐷 “ (0[,)𝑎)) → (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
4342adantl 481 . . . . . . . . . . . . . 14 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
44 simp2 1082 . . . . . . . . . . . . . . . 16 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → 𝐷 ∈ (PsMet‘𝑋))
45 psmetf 22158 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
46 ffun 6086 . . . . . . . . . . . . . . . 16 (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun 𝐷)
47 respreima 6384 . . . . . . . . . . . . . . . 16 (Fun 𝐷 → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
4844, 45, 46, 474syl 19 . . . . . . . . . . . . . . 15 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
4948ad6antr 777 . . . . . . . . . . . . . 14 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
5043, 49eqtr4d 2688 . . . . . . . . . . . . 13 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
51 rspe 3032 . . . . . . . . . . . . 13 ((𝑎 ∈ ℝ+ ∧ (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) → ∃𝑎 ∈ ℝ+ (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
5241, 50, 51syl2anc 694 . . . . . . . . . . . 12 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → ∃𝑎 ∈ ℝ+ (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
53 vex 3234 . . . . . . . . . . . . . 14 𝑤 ∈ V
5453inex1 4832 . . . . . . . . . . . . 13 (𝑤 ∩ (𝐴 × 𝐴)) ∈ V
55 eqid 2651 . . . . . . . . . . . . . 14 (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) = (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
5655elrnmpt 5404 . . . . . . . . . . . . 13 ((𝑤 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ+ (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))))
5754, 56ax-mp 5 . . . . . . . . . . . 12 ((𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ+ (𝑤 ∩ (𝐴 × 𝐴)) = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
5852, 57sylibr 224 . . . . . . . . . . 11 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))))
59 simpllr 815 . . . . . . . . . . . . 13 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → 𝑤𝑣)
60 ssinss1 3874 . . . . . . . . . . . . 13 (𝑤𝑣 → (𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣)
6159, 60syl 17 . . . . . . . . . . . 12 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣)
62 inss2 3867 . . . . . . . . . . . . 13 (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
6362a1i 11 . . . . . . . . . . . 12 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴))
64 pweq 4194 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝒫 𝑢 = 𝒫 (𝑣 ∩ (𝐴 × 𝐴)))
6564eleq2d 2716 . . . . . . . . . . . . . . 15 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ (𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 × 𝐴))))
6654elpw 4197 . . . . . . . . . . . . . . 15 ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 × 𝐴)) ↔ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝑣 ∩ (𝐴 × 𝐴)))
6765, 66syl6bb 276 . . . . . . . . . . . . . 14 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝑣 ∩ (𝐴 × 𝐴))))
68 ssin 3868 . . . . . . . . . . . . . 14 (((𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣 ∧ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)) ↔ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝑣 ∩ (𝐴 × 𝐴)))
6967, 68syl6bbr 278 . . . . . . . . . . . . 13 (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ ((𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣 ∧ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴))))
7069ad5antlr 775 . . . . . . . . . . . 12 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ ((𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣 ∧ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴))))
7161, 63, 70mpbir2and 977 . . . . . . . . . . 11 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢)
72 inelcm 4065 . . . . . . . . . . 11 (((𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∧ (𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢) → (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
7358, 71, 72syl2anc 694 . . . . . . . . . 10 ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) ∧ 𝑎 ∈ ℝ+) ∧ 𝑤 = (𝐷 “ (0[,)𝑎))) → (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
74 simplr 807 . . . . . . . . . . 11 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) → 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))))
75 eqid 2651 . . . . . . . . . . . . 13 (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
7675elrnmpt 5404 . . . . . . . . . . . 12 (𝑤 ∈ V → (𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎))))
7753, 76ax-mp 5 . . . . . . . . . . 11 (𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)))
7874, 77sylib 208 . . . . . . . . . 10 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)))
7934, 40, 73, 78r19.29af2 3104 . . . . . . . . 9 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))) ∧ 𝑤𝑣) → (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
80 ssn0 4009 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐴 ≠ ∅) → 𝑋 ≠ ∅)
8180ancoms 468 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ 𝐴𝑋) → 𝑋 ≠ ∅)
82813adant2 1100 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → 𝑋 ≠ ∅)
83 metuel 22416 . . . . . . . . . . . 12 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑣 ∈ (metUnif‘𝐷) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤𝑣)))
8482, 44, 83syl2anc 694 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (𝑣 ∈ (metUnif‘𝐷) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤𝑣)))
8584simplbda 653 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤𝑣)
8685adantr 480 . . . . . . . . 9 ((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤𝑣)
8779, 86r19.29a 3107 . . . . . . . 8 ((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
8887r19.29an 3106 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
8927, 88jca 553 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅))
90 simprl 809 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
9190elpwid 4203 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 ⊆ (𝐴 × 𝐴))
92 simpl3 1086 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝐴𝑋)
93 xpss12 5158 . . . . . . . . . . 11 ((𝐴𝑋𝐴𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
9492, 92, 93syl2anc 694 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
9591, 94sstrd 3646 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 ⊆ (𝑋 × 𝑋))
96 difssd 3771 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ⊆ (𝑋 × 𝑋))
9795, 96unssd 3822 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ (𝑋 × 𝑋))
98 simplr 807 . . . . . . . . . . . 12 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑏 ∈ ℝ+)
99 eqidd 2652 . . . . . . . . . . . 12 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑏)))
1004imaeq2d 5501 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)𝑏)))
101100eqeq2d 2661 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → ((𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑎)) ↔ (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑏))))
102101rspcev 3340 . . . . . . . . . . . 12 ((𝑏 ∈ ℝ+ ∧ (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑏))) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑎)))
10398, 99, 102syl2anc 694 . . . . . . . . . . 11 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑎)))
10444ad4antr 769 . . . . . . . . . . . 12 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝐷 ∈ (PsMet‘𝑋))
105 cnvexg 7154 . . . . . . . . . . . 12 (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V)
106 imaexg 7145 . . . . . . . . . . . 12 (𝐷 ∈ V → (𝐷 “ (0[,)𝑏)) ∈ V)
10775elrnmpt 5404 . . . . . . . . . . . 12 ((𝐷 “ (0[,)𝑏)) ∈ V → ((𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑎))))
108104, 105, 106, 1074syl 19 . . . . . . . . . . 11 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)𝑎))))
109103, 108mpbird 247 . . . . . . . . . 10 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))))
110 cnvimass 5520 . . . . . . . . . . . . . . . 16 (𝐷 “ (0[,)𝑏)) ⊆ dom 𝐷
111 fdm 6089 . . . . . . . . . . . . . . . . 17 (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom 𝐷 = (𝑋 × 𝑋))
11245, 111syl 17 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
113110, 112syl5sseq 3686 . . . . . . . . . . . . . . 15 (𝐷 ∈ (PsMet‘𝑋) → (𝐷 “ (0[,)𝑏)) ⊆ (𝑋 × 𝑋))
114104, 113syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (𝐷 “ (0[,)𝑏)) ⊆ (𝑋 × 𝑋))
115 ssdif0 3975 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)𝑏)) ⊆ (𝑋 × 𝑋) ↔ ((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) = ∅)
116114, 115sylib 208 . . . . . . . . . . . . 13 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) = ∅)
117 0ss 4005 . . . . . . . . . . . . 13 ∅ ⊆ 𝑢
118116, 117syl6eqss 3688 . . . . . . . . . . . 12 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ⊆ 𝑢)
119 respreima 6384 . . . . . . . . . . . . . 14 (Fun 𝐷 → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) = ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)))
120104, 45, 46, 1194syl 19 . . . . . . . . . . . . 13 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) = ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)))
121 simpr 476 . . . . . . . . . . . . . 14 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
122 simpllr 815 . . . . . . . . . . . . . . 15 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑣 ∈ 𝒫 𝑢)
123122elpwid 4203 . . . . . . . . . . . . . 14 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑣𝑢)
124121, 123eqsstr3d 3673 . . . . . . . . . . . . 13 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ⊆ 𝑢)
125120, 124eqsstr3d 3673 . . . . . . . . . . . 12 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)) ⊆ 𝑢)
126118, 125unssd 3822 . . . . . . . . . . 11 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
127 ssundif 4085 . . . . . . . . . . . 12 ((𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ↔ ((𝐷 “ (0[,)𝑏)) ∖ 𝑢) ⊆ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)))
128 difcom 4086 . . . . . . . . . . . 12 (((𝐷 “ (0[,)𝑏)) ∖ 𝑢) ⊆ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ↔ ((𝐷 “ (0[,)𝑏)) ∖ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ 𝑢)
129 difdif2 3917 . . . . . . . . . . . . 13 ((𝐷 “ (0[,)𝑏)) ∖ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) = (((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)))
130129sseq1i 3662 . . . . . . . . . . . 12 (((𝐷 “ (0[,)𝑏)) ∖ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ 𝑢 ↔ (((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
131127, 128, 1303bitri 286 . . . . . . . . . . 11 ((𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ↔ (((𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
132126, 131sylibr 224 . . . . . . . . . 10 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
133 sseq1 3659 . . . . . . . . . . 11 (𝑤 = (𝐷 “ (0[,)𝑏)) → (𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ↔ (𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)))))
134133rspcev 3340 . . . . . . . . . 10 (((𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ∧ (𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)))) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
135109, 132, 134syl2anc 694 . . . . . . . . 9 ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ+) ∧ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
136 elin 3829 . . . . . . . . . . . . . 14 (𝑣 ∈ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ↔ (𝑣 ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∧ 𝑣 ∈ 𝒫 𝑢))
137 vex 3234 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
1386elrnmpt 5404 . . . . . . . . . . . . . . . 16 (𝑣 ∈ V → (𝑣 ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
139137, 138ax-mp 5 . . . . . . . . . . . . . . 15 (𝑣 ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
140139anbi1i 731 . . . . . . . . . . . . . 14 ((𝑣 ∈ ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∧ 𝑣 ∈ 𝒫 𝑢) ↔ (∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑢))
141 ancom 465 . . . . . . . . . . . . . 14 ((∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑢) ↔ (𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
142136, 140, 1413bitri 286 . . . . . . . . . . . . 13 (𝑣 ∈ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ↔ (𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
143142exbii 1814 . . . . . . . . . . . 12 (∃𝑣 𝑣 ∈ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ↔ ∃𝑣(𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
144 n0 3964 . . . . . . . . . . . 12 ((ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢))
145 df-rex 2947 . . . . . . . . . . . 12 (∃𝑣 ∈ 𝒫 𝑢𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ↔ ∃𝑣(𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
146143, 144, 1453bitr4i 292 . . . . . . . . . . 11 ((ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑣 ∈ 𝒫 𝑢𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
147146biimpi 206 . . . . . . . . . 10 ((ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅ → ∃𝑣 ∈ 𝒫 𝑢𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
148147ad2antll 765 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ∃𝑣 ∈ 𝒫 𝑢𝑏 ∈ ℝ+ 𝑣 = ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
149135, 148r19.29vva 3110 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
15082adantr 480 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑋 ≠ ∅)
15144adantr 480 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝐷 ∈ (PsMet‘𝑋))
152 metuel 22416 . . . . . . . . 9 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷) ↔ ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))))
153150, 151, 152syl2anc 694 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷) ↔ ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))))
15497, 149, 153mpbir2and 977 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷))
155 indir 3908 . . . . . . . . 9 ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∪ (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴)))
156 incom 3838 . . . . . . . . . . 11 ((𝐴 × 𝐴) ∩ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) = (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴))
157 disjdif 4073 . . . . . . . . . . 11 ((𝐴 × 𝐴) ∩ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) = ∅
158156, 157eqtr3i 2675 . . . . . . . . . 10 (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴)) = ∅
159158uneq2i 3797 . . . . . . . . 9 ((𝑢 ∩ (𝐴 × 𝐴)) ∪ (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴))) = ((𝑢 ∩ (𝐴 × 𝐴)) ∪ ∅)
160 un0 4000 . . . . . . . . 9 ((𝑢 ∩ (𝐴 × 𝐴)) ∪ ∅) = (𝑢 ∩ (𝐴 × 𝐴))
161155, 159, 1603eqtri 2677 . . . . . . . 8 ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴))
162 df-ss 3621 . . . . . . . . 9 (𝑢 ⊆ (𝐴 × 𝐴) ↔ (𝑢 ∩ (𝐴 × 𝐴)) = 𝑢)
16391, 162sylib 208 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝑢 ∩ (𝐴 × 𝐴)) = 𝑢)
164161, 163syl5req 2698 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)))
165 ineq1 3840 . . . . . . . . 9 (𝑣 = (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) → (𝑣 ∩ (𝐴 × 𝐴)) = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)))
166165eqeq2d 2661 . . . . . . . 8 (𝑣 = (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) → (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) ↔ 𝑢 = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴))))
167166rspcev 3340 . . . . . . 7 (((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷) ∧ 𝑢 = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴))) → ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
168154, 164, 167syl2anc 694 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
16989, 168impbida 895 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) ↔ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)))
170 eqid 2651 . . . . . . 7 (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) = (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴)))
171170elrnmpt 5404 . . . . . 6 (𝑢 ∈ V → (𝑢 ∈ ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) ↔ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))))
17223, 171ax-mp 5 . . . . 5 (𝑢 ∈ ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) ↔ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
173 pweq 4194 . . . . . . . 8 (𝑣 = 𝑢 → 𝒫 𝑣 = 𝒫 𝑢)
174173ineq2d 3847 . . . . . . 7 (𝑣 = 𝑢 → (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) = (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢))
175174neeq1d 2882 . . . . . 6 (𝑣 = 𝑢 → ((ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅ ↔ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅))
176175elrab 3396 . . . . 5 (𝑢 ∈ {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅} ↔ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅))
177169, 172, 1763bitr4g 303 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (𝑢 ∈ ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) ↔ 𝑢 ∈ {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅}))
178177eqrdv 2649 . . 3 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
17919, 178eqtrd 2685 . 2 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ((metUnif‘𝐷) ↾t (𝐴 × 𝐴)) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ+ ↦ ((𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
18011, 13, 1793eqtr4rd 2696 1 ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → ((metUnif‘𝐷) ↾t (𝐴 × 𝐴)) = (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wne 2823  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Fun wfun 5920  wf 5922  cfv 5926  (class class class)co 6690  0cc0 9974  *cxr 10111  +crp 11870  [,)cico 12215  t crest 16128  PsMetcpsmet 19778  fBascfbas 19782  filGencfg 19783  metUnifcmetu 19785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-rp 11871  df-ico 12219  df-rest 16130  df-psmet 19786  df-fbas 19791  df-fg 19792  df-metu 19793
This theorem is referenced by:  reust  23215  qqhucn  30164
  Copyright terms: Public domain W3C validator