Metamath Proof Explorer

Theorem cncfioobdlem

Description: G actually extends F . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfioobdlem.a ⊢ φ → A ∈ ℝ
cncfioobdlem.b ⊢ φ → B ∈ ℝ
cncfioobdlem.f ⊢ φ → F : A B ⟶ V
cncfioobdlem.g ⊢ G = x ∈ A B ⟼ if x = A R if x = B L F ⁡ x
cncfioobdlem.c ⊢ φ → C ∈ A B
Assertion cncfioobdlem ⊢ φ → G ⁡ C = F ⁡ C

Proof

Step Hyp Ref Expression
1 cncfioobdlem.a ⊢ φ → A ∈ ℝ
2 cncfioobdlem.b ⊢ φ → B ∈ ℝ
3 cncfioobdlem.f ⊢ φ → F : A B ⟶ V
4 cncfioobdlem.g ⊢ G = x ∈ A B ⟼ if x = A R if x = B L F ⁡ x
5 cncfioobdlem.c ⊢ φ → C ∈ A B
6 4 a1i ⊢ φ → G = x ∈ A B ⟼ if x = A R if x = B L F ⁡ x
7 1 adantr ⊢ φ ∧ x = C → A ∈ ℝ
8 1 rexrd ⊢ φ → A ∈ ℝ *
9 2 rexrd ⊢ φ → B ∈ ℝ *
10 elioo2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C < B
11 8 9 10 syl2anc ⊢ φ → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C < B
12 5 11 mpbid ⊢ φ → C ∈ ℝ ∧ A < C ∧ C < B
13 12 simp2d ⊢ φ → A < C
14 13 adantr ⊢ φ ∧ x = C → A < C
15 eqcom ⊢ x = C ↔ C = x
16 15 bilani ⊢ φ ∧ x = C → C = x
17 14 16 breqtrd ⊢ φ ∧ x = C → A < x
18 7 17 gtned ⊢ φ ∧ x = C → x ≠ A
19 18 neneqd ⊢ φ ∧ x = C → ¬ x = A
20 19 iffalsed ⊢ φ ∧ x = C → if x = A R if x = B L F ⁡ x = if x = B L F ⁡ x
21 simpr ⊢ φ ∧ x = C → x = C
22 5 elioored ⊢ φ → C ∈ ℝ
23 22 adantr ⊢ φ ∧ x = C → C ∈ ℝ
24 21 23 eqeltrd ⊢ φ ∧ x = C → x ∈ ℝ
25 12 simp3d ⊢ φ → C < B
26 25 adantr ⊢ φ ∧ x = C → C < B
27 21 26 eqbrtrd ⊢ φ ∧ x = C → x < B
28 24 27 ltned ⊢ φ ∧ x = C → x ≠ B
29 28 neneqd ⊢ φ ∧ x = C → ¬ x = B
30 29 iffalsed ⊢ φ ∧ x = C → if x = B L F ⁡ x = F ⁡ x
31 21 fveq2d ⊢ φ ∧ x = C → F ⁡ x = F ⁡ C
32 20 30 31 3eqtrd ⊢ φ ∧ x = C → if x = A R if x = B L F ⁡ x = F ⁡ C
33 ioossicc ⊢ A B ⊆ A B
34 33 5 sselid ⊢ φ → C ∈ A B
35 3 5 ffvelcdmd ⊢ φ → F ⁡ C ∈ V
36 6 32 34 35 fvmptd ⊢ φ → G ⁡ C = F ⁡ C