Metamath Proof Explorer

Theorem i1fposd

Description: Deduction form of i1fposd . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis i1fposd.1 ⊢ φ → x ∈ ℝ ⟼ A ∈ dom ⁡ ∫ 1
Assertion i1fposd ⊢ φ → x ∈ ℝ ⟼ if 0 ≤ A A 0 ∈ dom ⁡ ∫ 1

Proof

Step Hyp Ref Expression
1 i1fposd.1 ⊢ φ → x ∈ ℝ ⟼ A ∈ dom ⁡ ∫ 1
2 nfcv ⊢ Ⅎ _ x 0
3 nfcv ⊢ Ⅎ _ x ≤
4 nffvmpt1 ⊢ Ⅎ _ x x ∈ ℝ ⟼ A ⁡ y
5 2 3 4 nfbr ⊢ Ⅎ x 0 ≤ x ∈ ℝ ⟼ A ⁡ y
6 5 4 2 nfif ⊢ Ⅎ _ x if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0
7 nfcv ⊢ Ⅎ _ y if 0 ≤ x ∈ ℝ ⟼ A ⁡ x x ∈ ℝ ⟼ A ⁡ x 0
8 fveq2 ⊢ y = x → x ∈ ℝ ⟼ A ⁡ y = x ∈ ℝ ⟼ A ⁡ x
9 8 breq2d ⊢ y = x → 0 ≤ x ∈ ℝ ⟼ A ⁡ y ↔ 0 ≤ x ∈ ℝ ⟼ A ⁡ x
10 9 8 ifbieq1d ⊢ y = x → if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0 = if 0 ≤ x ∈ ℝ ⟼ A ⁡ x x ∈ ℝ ⟼ A ⁡ x 0
11 6 7 10 cbvmpt ⊢ y ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0 = x ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ x x ∈ ℝ ⟼ A ⁡ x 0
12 simpr ⊢ φ ∧ x ∈ ℝ → x ∈ ℝ
13 i1ff ⊢ x ∈ ℝ ⟼ A ∈ dom ⁡ ∫ 1 → x ∈ ℝ ⟼ A : ℝ ⟶ ℝ
14 1 13 syl ⊢ φ → x ∈ ℝ ⟼ A : ℝ ⟶ ℝ
15 14 fvmptelrn ⊢ φ ∧ x ∈ ℝ → A ∈ ℝ
16 eqid ⊢ x ∈ ℝ ⟼ A = x ∈ ℝ ⟼ A
17 16 fvmpt2 ⊢ x ∈ ℝ ∧ A ∈ ℝ → x ∈ ℝ ⟼ A ⁡ x = A
18 12 15 17 syl2anc ⊢ φ ∧ x ∈ ℝ → x ∈ ℝ ⟼ A ⁡ x = A
19 18 breq2d ⊢ φ ∧ x ∈ ℝ → 0 ≤ x ∈ ℝ ⟼ A ⁡ x ↔ 0 ≤ A
20 19 18 ifbieq1d ⊢ φ ∧ x ∈ ℝ → if 0 ≤ x ∈ ℝ ⟼ A ⁡ x x ∈ ℝ ⟼ A ⁡ x 0 = if 0 ≤ A A 0
21 20 mpteq2dva ⊢ φ → x ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ x x ∈ ℝ ⟼ A ⁡ x 0 = x ∈ ℝ ⟼ if 0 ≤ A A 0
22 11 21 syl5eq ⊢ φ → y ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0 = x ∈ ℝ ⟼ if 0 ≤ A A 0
23 eqid ⊢ y ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0 = y ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0
24 23 i1fpos ⊢ x ∈ ℝ ⟼ A ∈ dom ⁡ ∫ 1 → y ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0 ∈ dom ⁡ ∫ 1
25 1 24 syl ⊢ φ → y ∈ ℝ ⟼ if 0 ≤ x ∈ ℝ ⟼ A ⁡ y x ∈ ℝ ⟼ A ⁡ y 0 ∈ dom ⁡ ∫ 1
26 22 25 eqeltrrd ⊢ φ → x ∈ ℝ ⟼ if 0 ≤ A A 0 ∈ dom ⁡ ∫ 1