Theorem isxmet

Description: Express the predicate " D is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	isxmet	⊢ ( 𝑋 ∈ 𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ V )
2		xpeq12	⊢ ( ( 𝑡 = 𝑋 ∧ 𝑡 = 𝑋 ) → ( 𝑡 × 𝑡 ) = ( 𝑋 × 𝑋 ) )
3	2	anidms	⊢ ( 𝑡 = 𝑋 → ( 𝑡 × 𝑡 ) = ( 𝑋 × 𝑋 ) )
4	3	oveq2d	⊢ ( 𝑡 = 𝑋 → ( ℝ* ↑m ( 𝑡 × 𝑡 ) ) = ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) )
5		raleq	⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑧 ∈ 𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) )
6	5	anbi2d	⊢ ( 𝑡 = 𝑋 → ( ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
7	6	raleqbi1dv	⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑦 ∈ 𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
8	7	raleqbi1dv	⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
9	4 8	rabeqbidv	⊢ ( 𝑡 = 𝑋 → { 𝑑 ∈ ( ℝ* ↑m ( 𝑡 × 𝑡 ) ) ∣ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } = { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
10		df-xmet	⊢ ∞Met = ( 𝑡 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑡 × 𝑡 ) ) ∣ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
11		ovex	⊢ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∈ V
12	11	rabex	⊢ { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ∈ V
13	9 10 12	fvmpt	⊢ ( 𝑋 ∈ V → ( ∞Met ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
14	1 13	syl	⊢ ( 𝑋 ∈ 𝐴 → ( ∞Met ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
15	14	eleq2d	⊢ ( 𝑋 ∈ 𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ 𝐷 ∈ { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ) )
16		oveq	⊢ ( 𝑑 = 𝐷 → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
17	16	eqeq1d	⊢ ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ ( 𝑥 𝐷 𝑦 ) = 0 ) )
18	17	bibi1d	⊢ ( 𝑑 = 𝐷 → ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ) )
19		oveq	⊢ ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑥 ) = ( 𝑧 𝐷 𝑥 ) )
20		oveq	⊢ ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑦 ) = ( 𝑧 𝐷 𝑦 ) )
21	19 20	oveq12d	⊢ ( 𝑑 = 𝐷 → ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
22	16 21	breq12d	⊢ ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
23	22	ralbidv	⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
24	18 23	anbi12d	⊢ ( 𝑑 = 𝐷 → ( ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
25	24	2ralbidv	⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
26	25	elrab	⊢ ( 𝐷 ∈ { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ↔ ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
27	15 26	bitrdi	⊢ ( 𝑋 ∈ 𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
28		xrex	⊢ ℝ* ∈ V
29		sqxpexg	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 × 𝑋 ) ∈ V )
30		elmapg	⊢ ( ( ℝ* ∈ V ∧ ( 𝑋 × 𝑋 ) ∈ V ) → ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ) )
31	28 29 30	sylancr	⊢ ( 𝑋 ∈ 𝐴 → ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ) )
32	31	anbi1d	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
33	27 32	bitrd	⊢ ( 𝑋 ∈ 𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )