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