Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  metideq Structured version   Visualization version   GIF version

Theorem metideq 30064
Description: Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
Assertion
Ref Expression
metideq ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹))

Proof of Theorem metideq
StepHypRef Expression
1 simpl 472 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐷 ∈ (PsMet‘𝑋))
2 metidss 30062 . . . . . . . . 9 (𝐷 ∈ (PsMet‘𝑋) → (~Met𝐷) ⊆ (𝑋 × 𝑋))
3 dmss 5355 . . . . . . . . 9 ((~Met𝐷) ⊆ (𝑋 × 𝑋) → dom (~Met𝐷) ⊆ dom (𝑋 × 𝑋))
42, 3syl 17 . . . . . . . 8 (𝐷 ∈ (PsMet‘𝑋) → dom (~Met𝐷) ⊆ dom (𝑋 × 𝑋))
5 dmxpid 5377 . . . . . . . 8 dom (𝑋 × 𝑋) = 𝑋
64, 5syl6sseq 3684 . . . . . . 7 (𝐷 ∈ (PsMet‘𝑋) → dom (~Met𝐷) ⊆ 𝑋)
71, 6syl 17 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → dom (~Met𝐷) ⊆ 𝑋)
8 xpss 5159 . . . . . . . . . 10 (𝑋 × 𝑋) ⊆ (V × V)
92, 8syl6ss 3648 . . . . . . . . 9 (𝐷 ∈ (PsMet‘𝑋) → (~Met𝐷) ⊆ (V × V))
10 df-rel 5150 . . . . . . . . 9 (Rel (~Met𝐷) ↔ (~Met𝐷) ⊆ (V × V))
119, 10sylibr 224 . . . . . . . 8 (𝐷 ∈ (PsMet‘𝑋) → Rel (~Met𝐷))
121, 11syl 17 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → Rel (~Met𝐷))
13 simprl 809 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐴(~Met𝐷)𝐵)
14 releldm 5390 . . . . . . 7 ((Rel (~Met𝐷) ∧ 𝐴(~Met𝐷)𝐵) → 𝐴 ∈ dom (~Met𝐷))
1512, 13, 14syl2anc 694 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐴 ∈ dom (~Met𝐷))
167, 15sseldd 3637 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐴𝑋)
17 simprr 811 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐸(~Met𝐷)𝐹)
18 releldm 5390 . . . . . . 7 ((Rel (~Met𝐷) ∧ 𝐸(~Met𝐷)𝐹) → 𝐸 ∈ dom (~Met𝐷))
1912, 17, 18syl2anc 694 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐸 ∈ dom (~Met𝐷))
207, 19sseldd 3637 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐸𝑋)
21 psmetsym 22162 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐸𝑋) → (𝐴𝐷𝐸) = (𝐸𝐷𝐴))
221, 16, 20, 21syl3anc 1366 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐸𝐷𝐴))
23 psmetf 22158 . . . . . 6 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
2423fovrnda 6847 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸𝑋𝐴𝑋)) → (𝐸𝐷𝐴) ∈ ℝ*)
251, 20, 16, 24syl12anc 1364 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐸𝐷𝐴) ∈ ℝ*)
2622, 25eqeltrd 2730 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) ∈ ℝ*)
27 rnss 5386 . . . . . . . 8 ((~Met𝐷) ⊆ (𝑋 × 𝑋) → ran (~Met𝐷) ⊆ ran (𝑋 × 𝑋))
282, 27syl 17 . . . . . . 7 (𝐷 ∈ (PsMet‘𝑋) → ran (~Met𝐷) ⊆ ran (𝑋 × 𝑋))
29 rnxpid 5602 . . . . . . 7 ran (𝑋 × 𝑋) = 𝑋
3028, 29syl6sseq 3684 . . . . . 6 (𝐷 ∈ (PsMet‘𝑋) → ran (~Met𝐷) ⊆ 𝑋)
311, 30syl 17 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ran (~Met𝐷) ⊆ 𝑋)
32 relelrn 5391 . . . . . 6 ((Rel (~Met𝐷) ∧ 𝐴(~Met𝐷)𝐵) → 𝐵 ∈ ran (~Met𝐷))
3312, 13, 32syl2anc 694 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐵 ∈ ran (~Met𝐷))
3431, 33sseldd 3637 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐵𝑋)
3523fovrnda 6847 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵𝑋𝐸𝑋)) → (𝐵𝐷𝐸) ∈ ℝ*)
361, 34, 20, 35syl12anc 1364 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐸) ∈ ℝ*)
37 relelrn 5391 . . . . . . 7 ((Rel (~Met𝐷) ∧ 𝐸(~Met𝐷)𝐹) → 𝐹 ∈ ran (~Met𝐷))
3812, 17, 37syl2anc 694 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐹 ∈ ran (~Met𝐷))
3931, 38sseldd 3637 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → 𝐹𝑋)
40 psmetsym 22162 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐹𝑋𝐵𝑋) → (𝐹𝐷𝐵) = (𝐵𝐷𝐹))
411, 39, 34, 40syl3anc 1366 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐹𝐷𝐵) = (𝐵𝐷𝐹))
4223fovrnda 6847 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐹𝑋𝐵𝑋)) → (𝐹𝐷𝐵) ∈ ℝ*)
431, 39, 34, 42syl12anc 1364 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐹𝐷𝐵) ∈ ℝ*)
4441, 43eqeltrrd 2731 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐹) ∈ ℝ*)
45 psmettri2 22161 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵𝑋𝐴𝑋𝐸𝑋)) → (𝐴𝐷𝐸) ≤ ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸)))
461, 34, 16, 20, 45syl13anc 1368 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) ≤ ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸)))
47 psmetsym 22162 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
481, 16, 34, 47syl3anc 1366 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
4916, 34jca 553 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝑋𝐵𝑋))
50 metidv 30063 . . . . . . . . 9 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴(~Met𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0))
5150biimpa 500 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ 𝐴(~Met𝐷)𝐵) → (𝐴𝐷𝐵) = 0)
521, 49, 13, 51syl21anc 1365 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐵) = 0)
5348, 52eqtr3d 2687 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐴) = 0)
5453oveq1d 6705 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸)) = (0 +𝑒 (𝐵𝐷𝐸)))
55 xaddid2 12111 . . . . . 6 ((𝐵𝐷𝐸) ∈ ℝ* → (0 +𝑒 (𝐵𝐷𝐸)) = (𝐵𝐷𝐸))
5636, 55syl 17 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (0 +𝑒 (𝐵𝐷𝐸)) = (𝐵𝐷𝐸))
5754, 56eqtrd 2685 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸)) = (𝐵𝐷𝐸))
5846, 57breqtrd 4711 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) ≤ (𝐵𝐷𝐸))
59 psmettri2 22161 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐹𝑋𝐵𝑋𝐸𝑋)) → (𝐵𝐷𝐸) ≤ ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸)))
601, 39, 34, 20, 59syl13anc 1368 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐸) ≤ ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸)))
61 psmetsym 22162 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐹𝑋𝐸𝑋) → (𝐹𝐷𝐸) = (𝐸𝐷𝐹))
621, 39, 20, 61syl3anc 1366 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐹𝐷𝐸) = (𝐸𝐷𝐹))
6320, 39jca 553 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐸𝑋𝐹𝑋))
64 metidv 30063 . . . . . . . . 9 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸𝑋𝐹𝑋)) → (𝐸(~Met𝐷)𝐹 ↔ (𝐸𝐷𝐹) = 0))
6564biimpa 500 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸𝑋𝐹𝑋)) ∧ 𝐸(~Met𝐷)𝐹) → (𝐸𝐷𝐹) = 0)
661, 63, 17, 65syl21anc 1365 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐸𝐷𝐹) = 0)
6762, 66eqtrd 2685 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐹𝐷𝐸) = 0)
6867oveq2d 6706 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸)) = ((𝐹𝐷𝐵) +𝑒 0))
69 xaddid1 12110 . . . . . 6 ((𝐹𝐷𝐵) ∈ ℝ* → ((𝐹𝐷𝐵) +𝑒 0) = (𝐹𝐷𝐵))
7043, 69syl 17 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐹𝐷𝐵) +𝑒 0) = (𝐹𝐷𝐵))
7168, 70, 413eqtrd 2689 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸)) = (𝐵𝐷𝐹))
7260, 71breqtrd 4711 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐸) ≤ (𝐵𝐷𝐹))
7326, 36, 44, 58, 72xrletrd 12031 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) ≤ (𝐵𝐷𝐹))
7423fovrnda 6847 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴𝑋𝐹𝑋)) → (𝐴𝐷𝐹) ∈ ℝ*)
751, 16, 39, 74syl12anc 1364 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐹) ∈ ℝ*)
76 psmettri2 22161 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴𝑋𝐵𝑋𝐹𝑋)) → (𝐵𝐷𝐹) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹)))
771, 16, 34, 39, 76syl13anc 1368 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐹) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹)))
7852oveq1d 6705 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹)) = (0 +𝑒 (𝐴𝐷𝐹)))
79 xaddid2 12111 . . . . . 6 ((𝐴𝐷𝐹) ∈ ℝ* → (0 +𝑒 (𝐴𝐷𝐹)) = (𝐴𝐷𝐹))
8075, 79syl 17 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (0 +𝑒 (𝐴𝐷𝐹)) = (𝐴𝐷𝐹))
8178, 80eqtrd 2685 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹)) = (𝐴𝐷𝐹))
8277, 81breqtrd 4711 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐹))
83 psmettri2 22161 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸𝑋𝐴𝑋𝐹𝑋)) → (𝐴𝐷𝐹) ≤ ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹)))
841, 20, 16, 39, 83syl13anc 1368 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐹) ≤ ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹)))
85 xaddid1 12110 . . . . . 6 ((𝐸𝐷𝐴) ∈ ℝ* → ((𝐸𝐷𝐴) +𝑒 0) = (𝐸𝐷𝐴))
8625, 85syl 17 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐸𝐷𝐴) +𝑒 0) = (𝐸𝐷𝐴))
8766oveq2d 6706 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹)) = ((𝐸𝐷𝐴) +𝑒 0))
8886, 87, 223eqtr4d 2695 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹)) = (𝐴𝐷𝐸))
8984, 88breqtrd 4711 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐹) ≤ (𝐴𝐷𝐸))
9044, 75, 26, 82, 89xrletrd 12031 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐸))
91 xrletri3 12023 . . 3 (((𝐴𝐷𝐸) ∈ ℝ* ∧ (𝐵𝐷𝐹) ∈ ℝ*) → ((𝐴𝐷𝐸) = (𝐵𝐷𝐹) ↔ ((𝐴𝐷𝐸) ≤ (𝐵𝐷𝐹) ∧ (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐸))))
9226, 44, 91syl2anc 694 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → ((𝐴𝐷𝐸) = (𝐵𝐷𝐹) ↔ ((𝐴𝐷𝐸) ≤ (𝐵𝐷𝐹) ∧ (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐸))))
9373, 90, 92mpbir2and 977 1 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝐵𝐸(~Met𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  wss 3607   class class class wbr 4685   × cxp 5141  dom cdm 5143  ran crn 5144  Rel wrel 5148  cfv 5926  (class class class)co 6690  0cc0 9974  *cxr 10111  cle 10113   +𝑒 cxad 11982  PsMetcpsmet 19778  ~Metcmetid 30057
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-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
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-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-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-ov 6693  df-oprab 6694  df-mpt2 6695  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-xadd 11985  df-psmet 19786  df-metid 30059
This theorem is referenced by:  pstmfval  30067
  Copyright terms: Public domain W3C validator