Metamath Proof Explorer

Theorem fourierdlem17

Description: The defined L is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem17.a ⊢ φ → A ∈ ℝ
fourierdlem17.b ⊢ φ → B ∈ ℝ
fourierdlem17.altb ⊢ φ → A < B
fourierdlem17.l ⊢ L = x ∈ A B ⟼ if x = B A x
Assertion fourierdlem17 ⊢ φ → L : A B ⟶ A B

Proof

Step Hyp Ref Expression
1 fourierdlem17.a ⊢ φ → A ∈ ℝ
2 fourierdlem17.b ⊢ φ → B ∈ ℝ
3 fourierdlem17.altb ⊢ φ → A < B
4 fourierdlem17.l ⊢ L = x ∈ A B ⟼ if x = B A x
5 1 leidd ⊢ φ → A ≤ A
6 1 2 3 ltled ⊢ φ → A ≤ B
7 1 2 1 5 6 eliccd ⊢ φ → A ∈ A B
8 7 ad2antrr ⊢ φ ∧ x ∈ A B ∧ x = B → A ∈ A B
9 iocssicc ⊢ A B ⊆ A B
10 9 sseli ⊢ x ∈ A B → x ∈ A B
11 10 ad2antlr ⊢ φ ∧ x ∈ A B ∧ ¬ x = B → x ∈ A B
12 8 11 ifclda ⊢ φ ∧ x ∈ A B → if x = B A x ∈ A B
13 12 4 fmptd ⊢ φ → L : A B ⟶ A B