Metamath Proof Explorer

Theorem reprinrn

Description: Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
Assertion reprinrn ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 fin ⊢ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ∧ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ) )
5 df-f ⊢ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ↔ ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ ran 𝑐 ⊆ 𝐵 ) )
6 ffn ⊢ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 → 𝑐 Fn ( 0 ..^ 𝑆 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) → 𝑐 Fn ( 0 ..^ 𝑆 ) )
8 7 biantrurd ⊢ ( ( 𝜑 ∧ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) → ( ran 𝑐 ⊆ 𝐵 ↔ ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ ran 𝑐 ⊆ 𝐵 ) ) )
9 8 bicomd ⊢ ( ( 𝜑 ∧ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) → ( ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ ran 𝑐 ⊆ 𝐵 ) ↔ ran 𝑐 ⊆ 𝐵 ) )
10 5 9 syl5bb ⊢ ( ( 𝜑 ∧ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) → ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ↔ ran 𝑐 ⊆ 𝐵 ) )
11 10 pm5.32da ⊢ ( 𝜑 → ( ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ∧ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 ) ↔ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ∧ ran 𝑐 ⊆ 𝐵 ) ) )
12 4 11 syl5bb ⊢ ( 𝜑 → ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ∧ ran 𝑐 ⊆ 𝐵 ) ) )
13 nnex ⊢ ℕ ∈ V
14 13 a1i ⊢ ( 𝜑 → ℕ ∈ V )
15 14 1 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
16 inex1g ⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ 𝐵 ) ∈ V )
17 15 16 syl ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ V )
18 ovex ⊢ ( 0 ..^ 𝑆 ) ∈ V
19 elmapg ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ 𝐵 ) ) )
20 17 18 19 sylancl ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ 𝐵 ) ) )
21 elmapg ⊢ ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
22 15 18 21 sylancl ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
23 22 anbi1d ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ran 𝑐 ⊆ 𝐵 ) ↔ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ∧ ran 𝑐 ⊆ 𝐵 ) ) )
24 12 20 23 3bitr4d ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ↔ ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ran 𝑐 ⊆ 𝐵 ) ) )
25 24 anbi1d ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ↔ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ran 𝑐 ⊆ 𝐵 ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ) )
26 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
27 26 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ℕ )
28 27 2 3 reprval ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
29 28 eleq2d ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ 𝑐 ∈ { 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ) )
30 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) )
31 29 30 bitrdi ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ) )
32 1 2 3 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
33 32 eleq2d ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ↔ 𝑐 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ) )
34 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) )
35 33 34 bitrdi ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ) )
36 35 anbi1d ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐵 ) ↔ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ∧ ran 𝑐 ⊆ 𝐵 ) ) )
37 an32 ⊢ ( ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ∧ ran 𝑐 ⊆ 𝐵 ) ↔ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ran 𝑐 ⊆ 𝐵 ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) )
38 36 37 bitrdi ⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐵 ) ↔ ( ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ ran 𝑐 ⊆ 𝐵 ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ) )
39 25 31 38 3bitr4d ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐵 ) ) )