Theorem shftfib

Description: Value of a fiber of the relation F . (Contributed by Mario Carneiro, 4-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	⊢ 𝐹 ∈ V
Assertion	shftfib	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	⊢ 𝐹 ∈ V
2	1	shftfval	⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
3	2	breqd	⊢ ( 𝐴 ∈ ℂ → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ 𝐵 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ) )
4		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
5		oveq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
6	5	breq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) )
7	4 6	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ) )
8		breq2	⊢ ( 𝑦 = 𝑧 → ( ( 𝐵 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) )
9	8	anbi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
10		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) }
11	7 9 10	brabg	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑧 ∈ V ) → ( 𝐵 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
12	11	elvd	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
13	3 12	sylan9bb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
14		ibar	⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 − 𝐴 ) 𝐹 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
15	14	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐹 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
16	13 15	bitr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) )
17	16	abbidv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } )
18		imasng	⊢ ( 𝐵 ∈ ℂ → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } )
19	18	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } )
20		ovex	⊢ ( 𝐵 − 𝐴 ) ∈ V
21		imasng	⊢ ( ( 𝐵 − 𝐴 ) ∈ V → ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } )
22	20 21	mp1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } )
23	17 19 22	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) )