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 biimpi ⊢ x = C → C = x
17 16 adantl ⊢ φ ∧ x = C → C = x
18 14 17 breqtrd ⊢ φ ∧ x = C → A < x
19 7 18 gtned ⊢ φ ∧ x = C → x ≠ A
20 19 neneqd ⊢ φ ∧ x = C → ¬ x = A
21 20 iffalsed ⊢ φ ∧ x = C → if x = A R if x = B L F ⁡ x = if x = B L F ⁡ x
22 simpr ⊢ φ ∧ x = C → x = C
23 5 elioored ⊢ φ → C ∈ ℝ
24 23 adantr ⊢ φ ∧ x = C → C ∈ ℝ
25 22 24 eqeltrd ⊢ φ ∧ x = C → x ∈ ℝ
26 12 simp3d ⊢ φ → C < B
27 26 adantr ⊢ φ ∧ x = C → C < B
28 22 27 eqbrtrd ⊢ φ ∧ x = C → x < B
29 25 28 ltned ⊢ φ ∧ x = C → x ≠ B
30 29 neneqd ⊢ φ ∧ x = C → ¬ x = B
31 30 iffalsed ⊢ φ ∧ x = C → if x = B L F ⁡ x = F ⁡ x
32 22 fveq2d ⊢ φ ∧ x = C → F ⁡ x = F ⁡ C
33 21 31 32 3eqtrd ⊢ φ ∧ x = C → if x = A R if x = B L F ⁡ x = F ⁡ C
34 ioossicc ⊢ A B ⊆ A B
35 34 5 sseldi ⊢ φ → C ∈ A B
36 3 5 ffvelrnd ⊢ φ → F ⁡ C ∈ V
37 6 33 35 36 fvmptd ⊢ φ → G ⁡ C = F ⁡ C