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

Theorem pstmfval 31846
Description: Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
pstmval.1 = (~Met𝐷)
Assertion
Ref Expression
pstmfval ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → ([𝐴] (pstoMet‘𝐷)[𝐵] ) = (𝐴𝐷𝐵))

Proof of Theorem pstmfval
Dummy variables 𝑎 𝑏 𝑥 𝑦 𝑧 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pstmval.1 . . . . 5 = (~Met𝐷)
21pstmval 31845 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)}))
323ad2ant1 1132 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)}))
43oveqd 7292 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → ([𝐴] (pstoMet‘𝐷)[𝐵] ) = ([𝐴] (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ))
51fvexi 6788 . . . . 5 ∈ V
65ecelqsi 8562 . . . 4 (𝐴𝑋 → [𝐴] ∈ (𝑋 / ))
763ad2ant2 1133 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → [𝐴] ∈ (𝑋 / ))
85ecelqsi 8562 . . . 4 (𝐵𝑋 → [𝐵] ∈ (𝑋 / ))
983ad2ant3 1134 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → [𝐵] ∈ (𝑋 / ))
10 rexeq 3343 . . . . . 6 (𝑥 = [𝐴] → (∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] 𝑏𝑦 𝑧 = (𝑎𝐷𝑏)))
1110abbidv 2807 . . . . 5 (𝑥 = [𝐴] → {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏𝑦 𝑧 = (𝑎𝐷𝑏)})
1211unieqd 4853 . . . 4 (𝑥 = [𝐴] {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏𝑦 𝑧 = (𝑎𝐷𝑏)})
13 rexeq 3343 . . . . . . 7 (𝑦 = [𝐵] → (∃𝑏𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)))
1413rexbidv 3226 . . . . . 6 (𝑦 = [𝐵] → (∃𝑎 ∈ [ 𝐴] 𝑏𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)))
1514abbidv 2807 . . . . 5 (𝑦 = [𝐵] → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)})
1615unieqd 4853 . . . 4 (𝑦 = [𝐵] {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)})
17 eqid 2738 . . . 4 (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)}) = (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)})
18 ecexg 8502 . . . . . . 7 ( ∈ V → [𝐴] ∈ V)
195, 18ax-mp 5 . . . . . 6 [𝐴] ∈ V
20 ecexg 8502 . . . . . . 7 ( ∈ V → [𝐵] ∈ V)
215, 20ax-mp 5 . . . . . 6 [𝐵] ∈ V
2219, 21ab2rexex 7822 . . . . 5 {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)} ∈ V
2322uniex 7594 . . . 4 {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)} ∈ V
2412, 16, 17, 23ovmpo 7433 . . 3 (([𝐴] ∈ (𝑋 / ) ∧ [𝐵] ∈ (𝑋 / )) → ([𝐴] (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ) = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)})
257, 9, 24syl2anc 584 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → ([𝐴] (𝑥 ∈ (𝑋 / ), 𝑦 ∈ (𝑋 / ) ↦ {𝑧 ∣ ∃𝑎𝑥𝑏𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ) = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)})
26 simpr3 1195 . . . . . . . . . . 11 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝑒𝐷𝑓))
27 simpl1 1190 . . . . . . . . . . . 12 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝐷 ∈ (PsMet‘𝑋))
28 simpr1 1193 . . . . . . . . . . . . . 14 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝑒 ∈ [𝐴] )
29 metidss 31841 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (PsMet‘𝑋) → (~Met𝐷) ⊆ (𝑋 × 𝑋))
301, 29eqsstrid 3969 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (PsMet‘𝑋) → ⊆ (𝑋 × 𝑋))
31 xpss 5605 . . . . . . . . . . . . . . . . . . 19 (𝑋 × 𝑋) ⊆ (V × V)
3230, 31sstrdi 3933 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ (PsMet‘𝑋) → ⊆ (V × V))
33 df-rel 5596 . . . . . . . . . . . . . . . . . 18 (Rel ⊆ (V × V))
3432, 33sylibr 233 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ (PsMet‘𝑋) → Rel )
35343ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → Rel )
3635adantr 481 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → Rel )
37 relelec 8543 . . . . . . . . . . . . . . 15 (Rel → (𝑒 ∈ [𝐴] 𝐴 𝑒))
3836, 37syl 17 . . . . . . . . . . . . . 14 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → (𝑒 ∈ [𝐴] 𝐴 𝑒))
3928, 38mpbid 231 . . . . . . . . . . . . 13 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝐴 𝑒)
401breqi 5080 . . . . . . . . . . . . 13 (𝐴 𝑒𝐴(~Met𝐷)𝑒)
4139, 40sylib 217 . . . . . . . . . . . 12 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝐴(~Met𝐷)𝑒)
42 simpr2 1194 . . . . . . . . . . . . . 14 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝑓 ∈ [𝐵] )
43 relelec 8543 . . . . . . . . . . . . . . 15 (Rel → (𝑓 ∈ [𝐵] 𝐵 𝑓))
4436, 43syl 17 . . . . . . . . . . . . . 14 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → (𝑓 ∈ [𝐵] 𝐵 𝑓))
4542, 44mpbid 231 . . . . . . . . . . . . 13 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝐵 𝑓)
461breqi 5080 . . . . . . . . . . . . 13 (𝐵 𝑓𝐵(~Met𝐷)𝑓)
4745, 46sylib 217 . . . . . . . . . . . 12 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝐵(~Met𝐷)𝑓)
48 metideq 31843 . . . . . . . . . . . 12 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met𝐷)𝑒𝐵(~Met𝐷)𝑓)) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓))
4927, 41, 47, 48syl12anc 834 . . . . . . . . . . 11 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓))
5026, 49eqtr4d 2781 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵))
5150adantlr 712 . . . . . . . . 9 ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)) ∧ (𝑒 ∈ [𝐴] 𝑓 ∈ [𝐵] 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵))
52513anassrs 1359 . . . . . . . 8 ((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)) ∧ 𝑒 ∈ [𝐴] ) ∧ 𝑓 ∈ [𝐵] ) ∧ 𝑧 = (𝑒𝐷𝑓)) → 𝑧 = (𝐴𝐷𝐵))
53 oveq1 7282 . . . . . . . . . . . 12 (𝑎 = 𝑒 → (𝑎𝐷𝑏) = (𝑒𝐷𝑏))
5453eqeq2d 2749 . . . . . . . . . . 11 (𝑎 = 𝑒 → (𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑏)))
55 oveq2 7283 . . . . . . . . . . . 12 (𝑏 = 𝑓 → (𝑒𝐷𝑏) = (𝑒𝐷𝑓))
5655eqeq2d 2749 . . . . . . . . . . 11 (𝑏 = 𝑓 → (𝑧 = (𝑒𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑓)))
5754, 56cbvrex2vw 3397 . . . . . . . . . 10 (∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑒 ∈ [ 𝐴] 𝑓 ∈ [ 𝐵] 𝑧 = (𝑒𝐷𝑓))
5857biimpi 215 . . . . . . . . 9 (∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏) → ∃𝑒 ∈ [ 𝐴] 𝑓 ∈ [ 𝐵] 𝑧 = (𝑒𝐷𝑓))
5958adantl 482 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)) → ∃𝑒 ∈ [ 𝐴] 𝑓 ∈ [ 𝐵] 𝑧 = (𝑒𝐷𝑓))
6052, 59r19.29vva 3266 . . . . . . 7 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)) → 𝑧 = (𝐴𝐷𝐵))
61 simpl1 1190 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐷 ∈ (PsMet‘𝑋))
62 simpl2 1191 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴𝑋)
63 psmet0 23461 . . . . . . . . . 10 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋) → (𝐴𝐷𝐴) = 0)
6461, 62, 63syl2anc 584 . . . . . . . . 9 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴𝐷𝐴) = 0)
65 relelec 8543 . . . . . . . . . . 11 (Rel → (𝐴 ∈ [𝐴] 𝐴 𝐴))
6661, 34, 653syl 18 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] 𝐴 𝐴))
671a1i 11 . . . . . . . . . . 11 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → = (~Met𝐷))
6867breqd 5085 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 𝐴𝐴(~Met𝐷)𝐴))
69 metidv 31842 . . . . . . . . . . 11 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴𝑋𝐴𝑋)) → (𝐴(~Met𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0))
7061, 62, 62, 69syl12anc 834 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴(~Met𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0))
7166, 68, 703bitrd 305 . . . . . . . . 9 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ↔ (𝐴𝐷𝐴) = 0))
7264, 71mpbird 256 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ [𝐴] )
73 simpl3 1192 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵𝑋)
74 psmet0 23461 . . . . . . . . . 10 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐵𝑋) → (𝐵𝐷𝐵) = 0)
7561, 73, 74syl2anc 584 . . . . . . . . 9 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵𝐷𝐵) = 0)
76 relelec 8543 . . . . . . . . . . 11 (Rel → (𝐵 ∈ [𝐵] 𝐵 𝐵))
7761, 34, 763syl 18 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] 𝐵 𝐵))
7867breqd 5085 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 𝐵𝐵(~Met𝐷)𝐵))
79 metidv 31842 . . . . . . . . . . 11 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵𝑋𝐵𝑋)) → (𝐵(~Met𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0))
8061, 73, 73, 79syl12anc 834 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵(~Met𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0))
8177, 78, 803bitrd 305 . . . . . . . . 9 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ↔ (𝐵𝐷𝐵) = 0))
8275, 81mpbird 256 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ [𝐵] )
83 simpr 485 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝑧 = (𝐴𝐷𝐵))
84 rspceov 7322 . . . . . . . 8 ((𝐴 ∈ [𝐴] 𝐵 ∈ [𝐵] 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏))
8572, 82, 83, 84syl3anc 1370 . . . . . . 7 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏))
8660, 85impbida 798 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝐴𝐷𝐵)))
8786abbidv 2807 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)} = {𝑧𝑧 = (𝐴𝐷𝐵)})
88 df-sn 4562 . . . . 5 {(𝐴𝐷𝐵)} = {𝑧𝑧 = (𝐴𝐷𝐵)}
8987, 88eqtr4di 2796 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)} = {(𝐴𝐷𝐵)})
9089unieqd 4853 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)} = {(𝐴𝐷𝐵)})
91 ovex 7308 . . . 4 (𝐴𝐷𝐵) ∈ V
9291unisn 4861 . . 3 {(𝐴𝐷𝐵)} = (𝐴𝐷𝐵)
9390, 92eqtrdi 2794 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] 𝑏 ∈ [ 𝐵] 𝑧 = (𝑎𝐷𝑏)} = (𝐴𝐷𝐵))
944, 25, 933eqtrd 2782 1 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → ([𝐴] (pstoMet‘𝐷)[𝐵] ) = (𝐴𝐷𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  {cab 2715  wrex 3065  Vcvv 3432  wss 3887  {csn 4561   cuni 4839   class class class wbr 5074   × cxp 5587  Rel wrel 5594  cfv 6433  (class class class)co 7275  cmpo 7277  [cec 8496   / cqs 8497  0cc0 10871  PsMetcpsmet 20581  ~Metcmetid 31836  pstoMetcpstm 31837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-er 8498  df-ec 8500  df-qs 8504  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-xadd 12849  df-psmet 20589  df-metid 31838  df-pstm 31839
This theorem is referenced by:  pstmxmet  31847
  Copyright terms: Public domain W3C validator