Metamath Proof Explorer


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 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵𝐴 ) } ) )