restmetu - Metamath Proof Explorer

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

Theorem restmetu 24560

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.

Step	Hyp	Ref	Expression
1		simp1 1142	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ≠ ∅)
2		psmetres2 24304	. . . . 5 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴))
3	2	3adant1 1136	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴))
4		oveq2 7371	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
5	4	imaeq2d 6019	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
6	5	cbvmptv 5183	. . . . . 6 ⊢ (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) = (𝑏 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
7	6	rneqi 5886	. . . . 5 ⊢ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
8	7	metustfbas 24547	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ (𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴)) → ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∈ (fBas‘(𝐴 × 𝐴)))
9	1, 3, 8	syl2anc 590	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∈ (fBas‘(𝐴 × 𝐴)))
10		fgval 23860	. . 3 ⊢ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∈ (fBas‘(𝐴 × 𝐴)) → ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
11	9, 10	syl 17	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
12		metuval 24539	. . 3 ⊢ ((𝐷 ↾ (𝐴 × 𝐴)) ∈ (PsMet‘𝐴) → (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))) = ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))))
13	3, 12	syl 17	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))) = ((𝐴 × 𝐴)filGenran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))))
14		fvex 6847	. . . 4 ⊢ (metUnif‘𝐷) ∈ V
15	3	elfvexd 6870	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
16	15, 15	xpexd 7701	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ∈ V)
17		restval 17387	. . . 4 ⊢ (((metUnif‘𝐷) ∈ V ∧ (𝐴 × 𝐴) ∈ V) → ((metUnif‘𝐷) ↾_t (𝐴 × 𝐴)) = ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))))
18	14, 16, 17	sylancr 593	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((metUnif‘𝐷) ↾_t (𝐴 × 𝐴)) = ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))))
19		inss2 4173	. . . . . . . . . . 11 ⊢ (𝑣 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
20		sseq1 3947	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → (𝑢 ⊆ (𝐴 × 𝐴) ↔ (𝑣 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)))
21	19, 20	mpbiri 259	. . . . . . . . . 10 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝑢 ⊆ (𝐴 × 𝐴))
22		vex 3436	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
23	22	elpw 4540	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑢 ⊆ (𝐴 × 𝐴))
24	21, 23	sylibr 235	. . . . . . . . 9 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
25	24	rexlimivw 3137	. . . . . . . 8 ⊢ (∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
26	25	adantl 482	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
27		nfv 1921	. . . . . . . . . . . 12 ⊢ Ⅎ𝑎(((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
28		nfmpt1 5178	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑎(𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
29	28	nfrn 5901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
30	29	nfcri 2894	. . . . . . . . . . . 12 ⊢ Ⅎ𝑎 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
31	27, 30	nfan 1906	. . . . . . . . . . 11 ⊢ Ⅎ𝑎((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))))
32		nfv 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑎 𝑤 ⊆ 𝑣
33	31, 32	nfan 1906	. . . . . . . . . 10 ⊢ Ⅎ𝑎(((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣)
34		nfmpt1 5178	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎(𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
35	34	nfrn 5901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑎ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
36		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑎𝒫 𝑢
37	35, 36	nfin 4160	. . . . . . . . . . 11 ⊢ Ⅎ𝑎(ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢)
38		nfcv 2902	. . . . . . . . . . 11 ⊢ Ⅎ𝑎∅
39	37, 38	nfne 3036	. . . . . . . . . 10 ⊢ Ⅎ𝑎(ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅
40		simplr 774	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ⁺)
41		ineq1 4149	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) → (𝑤 ∩ (𝐴 × 𝐴)) = ((^◡𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
42	41	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) = ((^◡𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
43		simp2 1143	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐷 ∈ (PsMet‘𝑋))
44		psmetf 24296	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
45		ffun 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → Fun 𝐷)
46		respreima 7014	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐷 → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((^◡𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
47	43, 44, 45, 46	4syl 19	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((^◡𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
48	47	ad6antr 742	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)) = ((^◡𝐷 “ (0[,)𝑎)) ∩ (𝐴 × 𝐴)))
49	42, 48	eqtr4d 2778	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
50		rspe 3230	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ⁺ ∧ (𝑤 ∩ (𝐴 × 𝐴)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) → ∃𝑎 ∈ ℝ⁺ (𝑤 ∩ (𝐴 × 𝐴)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
51	40, 49, 50	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑎 ∈ ℝ⁺ (𝑤 ∩ (𝐴 × 𝐴)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
52		vex 3436	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
53	52	inex1 5252	. . . . . . . . . . . . 13 ⊢ (𝑤 ∩ (𝐴 × 𝐴)) ∈ V
54		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) = (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
55	54	elrnmpt 5907	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ⁺ (𝑤 ∩ (𝐴 × 𝐴)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))))
56	53, 55	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ⁺ (𝑤 ∩ (𝐴 × 𝐴)) = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎)))
57	51, 56	sylibr 235	. . . . . . . . . . 11 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))))
58		simpllr 781	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → 𝑤 ⊆ 𝑣)
59		ssinss1 4181	. . . . . . . . . . . . 13 ⊢ (𝑤 ⊆ 𝑣 → (𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣)
60	58, 59	syl 17	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣)
61		inss2 4173	. . . . . . . . . . . . 13 ⊢ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
62	61	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴))
63		pweq 4550	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → 𝒫 𝑢 = 𝒫 (𝑣 ∩ (𝐴 × 𝐴)))
64	63	eleq2d 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ (𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 × 𝐴))))
65	53	elpw 4540	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 (𝑣 ∩ (𝐴 × 𝐴)) ↔ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝑣 ∩ (𝐴 × 𝐴)))
66	64, 65	bitrdi 288	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝑣 ∩ (𝐴 × 𝐴))))
67		ssin 4174	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣 ∧ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)) ↔ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝑣 ∩ (𝐴 × 𝐴)))
68	66, 67	bitr4di 290	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ ((𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣 ∧ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴))))
69	68	ad5antlr 741	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢 ↔ ((𝑤 ∩ (𝐴 × 𝐴)) ⊆ 𝑣 ∧ (𝑤 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴))))
70	60, 62, 69	mpbir2and 719	. . . . . . . . . . 11 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢)
71		inelcm 4400	. . . . . . . . . . 11 ⊢ (((𝑤 ∩ (𝐴 × 𝐴)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∧ (𝑤 ∩ (𝐴 × 𝐴)) ∈ 𝒫 𝑢) → (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
72	57, 70, 71	syl2anc 590	. . . . . . . . . 10 ⊢ ((((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑤 = (^◡𝐷 “ (0[,)𝑎))) → (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
73		simplr 774	. . . . . . . . . . 11 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))))
74		eqid 2740	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
75	74	elrnmpt 5907	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎))))
76	75	elv 3437	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
77	73, 76	sylib 219	. . . . . . . . . 10 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
78	33, 39, 72, 77	r19.29af2 3248	. . . . . . . . 9 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) ∧ 𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))) ∧ 𝑤 ⊆ 𝑣) → (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
79		ssn0 4339	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ≠ ∅) → 𝑋 ≠ ∅)
80	79	ancoms 459	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 𝑋) → 𝑋 ≠ ∅)
81	80	3adant2 1137	. . . . . . . . . . . 12 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ≠ ∅)
82		metuel 24554	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑣 ∈ (metUnif‘𝐷) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑣)))
83	81, 43, 82	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑣 ∈ (metUnif‘𝐷) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑣)))
84	83	simplbda 500	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑣)
85	84	adantr 481	. . . . . . . . 9 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑣)
86	78, 85	r19.29a 3148	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ 𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
87	86	r19.29an 3144	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)
88	26, 87	jca 516	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))) → (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅))
89		simprl 776	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 ∈ 𝒫 (𝐴 × 𝐴))
90	89	elpwid 4545	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 ⊆ (𝐴 × 𝐴))
91		simpl3 1200	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝐴 ⊆ 𝑋)
92		xpss12 5640	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
93	91, 91, 92	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
94	90, 93	sstrd 3932	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 ⊆ (𝑋 × 𝑋))
95		difssd 4074	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ⊆ (𝑋 × 𝑋))
96	94, 95	unssd 4128	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ (𝑋 × 𝑋))
97		simplr 774	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑏 ∈ ℝ⁺)
98		eqidd 2741	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)𝑏)))
99	4	imaeq2d 6019	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)𝑏)))
100	99	rspceeqv 3590	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)𝑏))) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)𝑎)))
101	97, 98, 100	syl2anc 590	. . . . . . . . . . 11 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)𝑎)))
102	43	ad4antr 738	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝐷 ∈ (PsMet‘𝑋))
103		cnvexg 7871	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ^◡𝐷 ∈ V)
104		imaexg 7860	. . . . . . . . . . . 12 ⊢ (^◡𝐷 ∈ V → (^◡𝐷 “ (0[,)𝑏)) ∈ V)
105	74	elrnmpt 5907	. . . . . . . . . . . 12 ⊢ ((^◡𝐷 “ (0[,)𝑏)) ∈ V → ((^◡𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)𝑎))))
106	102, 103, 104, 105	4syl 19	. . . . . . . . . . 11 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((^◡𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) ↔ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)𝑎))))
107	101, 106	mpbird 258	. . . . . . . . . 10 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))))
108		cnvimass 6041	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝐷 “ (0[,)𝑏)) ⊆ dom 𝐷
109	108, 44	fssdm 6681	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑋 × 𝑋))
110	102, 109	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑋 × 𝑋))
111		ssdif0 4301	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑋 × 𝑋) ↔ ((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) = ∅)
112	110, 111	sylib 219	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) = ∅)
113		0ss 4335	. . . . . . . . . . . . 13 ⊢ ∅ ⊆ 𝑢
114	112, 113	eqsstrdi 3966	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ⊆ 𝑢)
115		respreima 7014	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐷 → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) = ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)))
116	102, 44, 45, 115	4syl 19	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) = ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)))
117		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
118		simpllr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑣 ∈ 𝒫 𝑢)
119	118	elpwid 4545	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → 𝑣 ⊆ 𝑢)
120	117, 119	eqsstrrd 3957	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ⊆ 𝑢)
121	116, 120	eqsstrrd 3957	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)) ⊆ 𝑢)
122	114, 121	unssd 4128	. . . . . . . . . . 11 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
123		ssundif 4422	. . . . . . . . . . . 12 ⊢ ((^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ↔ ((^◡𝐷 “ (0[,)𝑏)) ∖ 𝑢) ⊆ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)))
124		difcom 4423	. . . . . . . . . . . 12 ⊢ (((^◡𝐷 “ (0[,)𝑏)) ∖ 𝑢) ⊆ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ↔ ((^◡𝐷 “ (0[,)𝑏)) ∖ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ 𝑢)
125		difdif2 4231	. . . . . . . . . . . . 13 ⊢ ((^◡𝐷 “ (0[,)𝑏)) ∖ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) = (((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴)))
126	125	sseq1i 3950	. . . . . . . . . . . 12 ⊢ (((^◡𝐷 “ (0[,)𝑏)) ∖ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ 𝑢 ↔ (((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
127	123, 124, 126	3bitri 298	. . . . . . . . . . 11 ⊢ ((^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ↔ (((^◡𝐷 “ (0[,)𝑏)) ∖ (𝑋 × 𝑋)) ∪ ((^◡𝐷 “ (0[,)𝑏)) ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
128	122, 127	sylibr 235	. . . . . . . . . 10 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
129		sseq1 3947	. . . . . . . . . . 11 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑏)) → (𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ↔ (^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)))))
130	129	rspcev 3567	. . . . . . . . . 10 ⊢ (((^◡𝐷 “ (0[,)𝑏)) ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) ∧ (^◡𝐷 “ (0[,)𝑏)) ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)))) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
131	107, 128, 130	syl2anc 590	. . . . . . . . 9 ⊢ ((((((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) ∧ 𝑣 ∈ 𝒫 𝑢) ∧ 𝑏 ∈ ℝ⁺) ∧ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
132		elin 3906	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ↔ (𝑣 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∧ 𝑣 ∈ 𝒫 𝑢))
133	6	elrnmpt 5907	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
134	133	elv 3437	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ↔ ∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
135	134	anbi1i 630	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∧ 𝑣 ∈ 𝒫 𝑢) ↔ (∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑢))
136		ancom 461	. . . . . . . . . . . . . 14 ⊢ ((∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ∧ 𝑣 ∈ 𝒫 𝑢) ↔ (𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
137	132, 135, 136	3bitri 298	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ↔ (𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
138	137	exbii 1855	. . . . . . . . . . . 12 ⊢ (∃𝑣 𝑣 ∈ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ↔ ∃𝑣(𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
139		n0 4288	. . . . . . . . . . . 12 ⊢ ((ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢))
140		df-rex 3065	. . . . . . . . . . . 12 ⊢ (∃𝑣 ∈ 𝒫 𝑢∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)) ↔ ∃𝑣(𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏))))
141	138, 139, 140	3bitr4i 304	. . . . . . . . . . 11 ⊢ ((ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑣 ∈ 𝒫 𝑢∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
142	141	biimpi 217	. . . . . . . . . 10 ⊢ ((ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅ → ∃𝑣 ∈ 𝒫 𝑢∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
143	142	ad2antll 735	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ∃𝑣 ∈ 𝒫 𝑢∃𝑏 ∈ ℝ⁺ 𝑣 = (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑏)))
144	131, 143	r19.29vva 3200	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))
145	81	adantr 481	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑋 ≠ ∅)
146	43	adantr 481	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝐷 ∈ (PsMet‘𝑋))
147		metuel 24554	. . . . . . . . 9 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷) ↔ ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))))
148	145, 146, 147	syl2anc 590	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷) ↔ ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))))))
149	96, 144, 148	mpbir2and 719	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷))
150		indir 4221	. . . . . . . . 9 ⊢ ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∪ (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴)))
151		disjdifr 4408	. . . . . . . . . 10 ⊢ (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴)) = ∅
152	151	uneq2i 4102	. . . . . . . . 9 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ∪ (((𝑋 × 𝑋) ∖ (𝐴 × 𝐴)) ∩ (𝐴 × 𝐴))) = ((𝑢 ∩ (𝐴 × 𝐴)) ∪ ∅)
153		un0 4329	. . . . . . . . 9 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ∪ ∅) = (𝑢 ∩ (𝐴 × 𝐴))
154	150, 152, 153	3eqtri 2767	. . . . . . . 8 ⊢ ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴))
155		dfss2 3908	. . . . . . . . 9 ⊢ (𝑢 ⊆ (𝐴 × 𝐴) ↔ (𝑢 ∩ (𝐴 × 𝐴)) = 𝑢)
156	90, 155	sylib 219	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → (𝑢 ∩ (𝐴 × 𝐴)) = 𝑢)
157	154, 156	eqtr2id 2788	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → 𝑢 = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)))
158		ineq1 4149	. . . . . . . 8 ⊢ (𝑣 = (𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) → (𝑣 ∩ (𝐴 × 𝐴)) = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴)))
159	158	rspceeqv 3590	. . . . . . 7 ⊢ (((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∈ (metUnif‘𝐷) ∧ 𝑢 = ((𝑢 ∪ ((𝑋 × 𝑋) ∖ (𝐴 × 𝐴))) ∩ (𝐴 × 𝐴))) → ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
160	149, 157, 159	syl2anc 590	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)) → ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
161	88, 160	impbida 806	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)) ↔ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅)))
162		eqid 2740	. . . . . . 7 ⊢ (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) = (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴)))
163	162	elrnmpt 5907	. . . . . 6 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) ↔ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴))))
164	163	elv 3437	. . . . 5 ⊢ (𝑢 ∈ ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) ↔ ∃𝑣 ∈ (metUnif‘𝐷)𝑢 = (𝑣 ∩ (𝐴 × 𝐴)))
165		pweq 4550	. . . . . . . 8 ⊢ (𝑣 = 𝑢 → 𝒫 𝑣 = 𝒫 𝑢)
166	165	ineq2d 4156	. . . . . . 7 ⊢ (𝑣 = 𝑢 → (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) = (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢))
167	166	neeq1d 2994	. . . . . 6 ⊢ (𝑣 = 𝑢 → ((ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅ ↔ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅))
168	167	elrab 3636	. . . . 5 ⊢ (𝑢 ∈ {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅} ↔ (𝑢 ∈ 𝒫 (𝐴 × 𝐴) ∧ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑢) ≠ ∅))
169	161, 164, 168	3bitr4g 315	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑢 ∈ ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) ↔ 𝑢 ∈ {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅}))
170	169	eqrdv 2738	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑣 ∈ (metUnif‘𝐷) ↦ (𝑣 ∩ (𝐴 × 𝐴))) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
171	18, 170	eqtrd 2775	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((metUnif‘𝐷) ↾_t (𝐴 × 𝐴)) = {𝑣 ∈ 𝒫 (𝐴 × 𝐴) ∣ (ran (𝑎 ∈ ℝ⁺ ↦ (^◡(𝐷 ↾ (𝐴 × 𝐴)) “ (0[,)𝑎))) ∩ 𝒫 𝑣) ≠ ∅})
172	11, 13, 171	3eqtr4rd 2786	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((metUnif‘𝐷) ↾_t (𝐴 × 𝐴)) = (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ≠ wne 2935 ∃wrex 3064 {crab 3392 Vcvv 3432 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4268 𝒫 cpw 4536 ↦ cmpt 5160 × cxp 5623 ^◡ccnv 5624 ran crn 5626 ↾ cres 5627 “ cima 5628 Fun wfun 6486 ⟶wf 6488 ‘cfv 6492 (class class class)co 7363 0cc0 11036 ℝ^*cxr 11176 ℝ⁺crp 12940 [,)cico 13298 ↾_t crest 17381 PsMetcpsmet 21338 fBascfbas 21342 filGencfg 21343 metUnifcmetu 21345

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-po 5533 df-so 5534 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-1st 7938 df-2nd 7939 df-er 8640 df-map 8772 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-rp 12941 df-ico 13302 df-rest 17383 df-psmet 21346 df-fbas 21351 df-fg 21352 df-metu 21353

This theorem is referenced by: reust 25373 qqhucn 34183

W3C validator