Metamath Proof Explorer

Theorem fliftval

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 ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = 𝐷 )

Proof

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 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = 𝐷 )