This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: The value of the function F . (Contributed by Mario Carneiro, 23-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | flift.1 | ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ 〈 𝐴 , 𝐵 〉 ) | |
| flift.2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 ) | ||
| flift.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 ) | ||
| fliftval.4 | ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐶 ) | ||
| fliftval.5 | ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 ) | ||
| fliftval.6 | ⊢ ( 𝜑 → Fun 𝐹 ) | ||
| Assertion | fliftval | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = 𝐷 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | flift.1 | ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ 〈 𝐴 , 𝐵 〉 ) | |
| 2 | flift.2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 ) | |
| 3 | flift.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 ) | |
| 4 | fliftval.4 | ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐶 ) | |
| 5 | fliftval.5 | ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 ) | |
| 6 | fliftval.6 | ⊢ ( 𝜑 → Fun 𝐹 ) | |
| 7 | 6 | adantr | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → Fun 𝐹 ) |
| 8 | simpr | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → 𝑌 ∈ 𝑋 ) | |
| 9 | eqidd | ⊢ ( 𝜑 → 𝐷 = 𝐷 ) | |
| 10 | eqidd | ⊢ ( 𝑌 ∈ 𝑋 → 𝐶 = 𝐶 ) | |
| 11 | 9 10 | anim12ci | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐶 = 𝐶 ∧ 𝐷 = 𝐷 ) ) |
| 12 | 4 | eqeq2d | ⊢ ( 𝑥 = 𝑌 → ( 𝐶 = 𝐴 ↔ 𝐶 = 𝐶 ) ) |
| 13 | 5 | eqeq2d | ⊢ ( 𝑥 = 𝑌 → ( 𝐷 = 𝐵 ↔ 𝐷 = 𝐷 ) ) |
| 14 | 12 13 | anbi12d | ⊢ ( 𝑥 = 𝑌 → ( ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐷 = 𝐷 ) ) ) |
| 15 | 14 | rspcev | ⊢ ( ( 𝑌 ∈ 𝑋 ∧ ( 𝐶 = 𝐶 ∧ 𝐷 = 𝐷 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) |
| 16 | 8 11 15 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) |
| 17 | 1 2 3 | fliftel | ⊢ ( 𝜑 → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) ) |
| 18 | 17 | adantr | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) ) |
| 19 | 16 18 | mpbird | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → 𝐶 𝐹 𝐷 ) |
| 20 | funbrfv | ⊢ ( Fun 𝐹 → ( 𝐶 𝐹 𝐷 → ( 𝐹 ‘ 𝐶 ) = 𝐷 ) ) | |
| 21 | 7 19 20 | sylc | ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = 𝐷 ) |