Metamath Proof Explorer


Theorem shftfn

Description: Functionality and domain of a sequence shifted by A . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 𝐹 ∈ V
Assertion shftfn ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ 𝐵 } )

Proof

Step Hyp Ref Expression
1 shftfval.1 𝐹 ∈ V
2 relopab Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) }
3 2 a1i ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } )
4 fnfun ( 𝐹 Fn 𝐵 → Fun 𝐹 )
5 4 adantr ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → Fun 𝐹 )
6 funmo ( Fun 𝐹 → ∃* 𝑤 ( 𝑧𝐴 ) 𝐹 𝑤 )
7 vex 𝑧 ∈ V
8 vex 𝑤 ∈ V
9 eleq1w ( 𝑥 = 𝑧 → ( 𝑥 ∈ ℂ ↔ 𝑧 ∈ ℂ ) )
10 oveq1 ( 𝑥 = 𝑧 → ( 𝑥𝐴 ) = ( 𝑧𝐴 ) )
11 10 breq1d ( 𝑥 = 𝑧 → ( ( 𝑥𝐴 ) 𝐹 𝑦 ↔ ( 𝑧𝐴 ) 𝐹 𝑦 ) )
12 9 11 anbi12d ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝑧𝐴 ) 𝐹 𝑦 ) ) )
13 breq2 ( 𝑦 = 𝑤 → ( ( 𝑧𝐴 ) 𝐹 𝑦 ↔ ( 𝑧𝐴 ) 𝐹 𝑤 ) )
14 13 anbi2d ( 𝑦 = 𝑤 → ( ( 𝑧 ∈ ℂ ∧ ( 𝑧𝐴 ) 𝐹 𝑦 ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝑧𝐴 ) 𝐹 𝑤 ) ) )
15 eqid { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) }
16 7 8 12 14 15 brab ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 ↔ ( 𝑧 ∈ ℂ ∧ ( 𝑧𝐴 ) 𝐹 𝑤 ) )
17 16 simprbi ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 → ( 𝑧𝐴 ) 𝐹 𝑤 )
18 17 moimi ( ∃* 𝑤 ( 𝑧𝐴 ) 𝐹 𝑤 → ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 )
19 6 18 syl ( Fun 𝐹 → ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 )
20 19 alrimiv ( Fun 𝐹 → ∀ 𝑧 ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 )
21 5 20 syl ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → ∀ 𝑧 ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 )
22 dffun6 ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } ↔ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } ∧ ∀ 𝑧 ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } 𝑤 ) )
23 3 21 22 sylanbrc ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } )
24 1 shftfval ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } )
25 24 adantl ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } )
26 25 funeqd ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → ( Fun ( 𝐹 shift 𝐴 ) ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥𝐴 ) 𝐹 𝑦 ) } ) )
27 23 26 mpbird ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → Fun ( 𝐹 shift 𝐴 ) )
28 1 shftdm ( 𝐴 ∈ ℂ → dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ dom 𝐹 } )
29 fndm ( 𝐹 Fn 𝐵 → dom 𝐹 = 𝐵 )
30 29 eleq2d ( 𝐹 Fn 𝐵 → ( ( 𝑥𝐴 ) ∈ dom 𝐹 ↔ ( 𝑥𝐴 ) ∈ 𝐵 ) )
31 30 rabbidv ( 𝐹 Fn 𝐵 → { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ dom 𝐹 } = { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ 𝐵 } )
32 28 31 sylan9eqr ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ 𝐵 } )
33 df-fn ( ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ 𝐵 } ↔ ( Fun ( 𝐹 shift 𝐴 ) ∧ dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ 𝐵 } ) )
34 27 32 33 sylanbrc ( ( 𝐹 Fn 𝐵𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥𝐴 ) ∈ 𝐵 } )