| Step | Hyp | Ref
| Expression |
| 1 | | fin 6788 |
. . . . 5
⊢ (𝑐:(0..^𝑆)⟶(𝐴 ∩ 𝐵) ↔ (𝑐:(0..^𝑆)⟶𝐴 ∧ 𝑐:(0..^𝑆)⟶𝐵)) |
| 2 | | df-f 6565 |
. . . . . . 7
⊢ (𝑐:(0..^𝑆)⟶𝐵 ↔ (𝑐 Fn (0..^𝑆) ∧ ran 𝑐 ⊆ 𝐵)) |
| 3 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝑐:(0..^𝑆)⟶𝐴 → 𝑐 Fn (0..^𝑆)) |
| 4 | 3 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐:(0..^𝑆)⟶𝐴) → 𝑐 Fn (0..^𝑆)) |
| 5 | 4 | biantrurd 532 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐:(0..^𝑆)⟶𝐴) → (ran 𝑐 ⊆ 𝐵 ↔ (𝑐 Fn (0..^𝑆) ∧ ran 𝑐 ⊆ 𝐵))) |
| 6 | 5 | bicomd 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐:(0..^𝑆)⟶𝐴) → ((𝑐 Fn (0..^𝑆) ∧ ran 𝑐 ⊆ 𝐵) ↔ ran 𝑐 ⊆ 𝐵)) |
| 7 | 2, 6 | bitrid 283 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐:(0..^𝑆)⟶𝐴) → (𝑐:(0..^𝑆)⟶𝐵 ↔ ran 𝑐 ⊆ 𝐵)) |
| 8 | 7 | pm5.32da 579 |
. . . . 5
⊢ (𝜑 → ((𝑐:(0..^𝑆)⟶𝐴 ∧ 𝑐:(0..^𝑆)⟶𝐵) ↔ (𝑐:(0..^𝑆)⟶𝐴 ∧ ran 𝑐 ⊆ 𝐵))) |
| 9 | 1, 8 | bitrid 283 |
. . . 4
⊢ (𝜑 → (𝑐:(0..^𝑆)⟶(𝐴 ∩ 𝐵) ↔ (𝑐:(0..^𝑆)⟶𝐴 ∧ ran 𝑐 ⊆ 𝐵))) |
| 10 | | nnex 12272 |
. . . . . . . 8
⊢ ℕ
∈ V |
| 11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ ∈
V) |
| 12 | | reprval.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
| 13 | 11, 12 | ssexd 5324 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
| 14 | | inex1g 5319 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) ∈ V) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ V) |
| 16 | | ovex 7464 |
. . . . 5
⊢
(0..^𝑆) ∈
V |
| 17 | | elmapg 8879 |
. . . . 5
⊢ (((𝐴 ∩ 𝐵) ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶(𝐴 ∩ 𝐵))) |
| 18 | 15, 16, 17 | sylancl 586 |
. . . 4
⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶(𝐴 ∩ 𝐵))) |
| 19 | | elmapg 8879 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
| 20 | 13, 16, 19 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
| 21 | 20 | anbi1d 631 |
. . . 4
⊢ (𝜑 → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ ran 𝑐 ⊆ 𝐵) ↔ (𝑐:(0..^𝑆)⟶𝐴 ∧ ran 𝑐 ⊆ 𝐵))) |
| 22 | 9, 18, 21 | 3bitr4d 311 |
. . 3
⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ↔ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ ran 𝑐 ⊆ 𝐵))) |
| 23 | 22 | anbi1d 631 |
. 2
⊢ (𝜑 → ((𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) ↔ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ ran 𝑐 ⊆ 𝐵) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀))) |
| 24 | | inss1 4237 |
. . . . . 6
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 25 | 24, 12 | sstrid 3995 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℕ) |
| 26 | | reprval.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 27 | | reprval.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
| 28 | 25, 26, 27 | reprval 34625 |
. . . 4
⊢ (𝜑 → ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) = {𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 29 | 28 | eleq2d 2827 |
. . 3
⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ 𝑐 ∈ {𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀})) |
| 30 | | rabid 3458 |
. . 3
⊢ (𝑐 ∈ {𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} ↔ (𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀)) |
| 31 | 29, 30 | bitrdi 287 |
. 2
⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ ((𝐴 ∩ 𝐵) ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀))) |
| 32 | 12, 26, 27 | reprval 34625 |
. . . . . 6
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 33 | 32 | eleq2d 2827 |
. . . . 5
⊢ (𝜑 → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ↔ 𝑐 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀})) |
| 34 | | rabid 3458 |
. . . . 5
⊢ (𝑐 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} ↔ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀)) |
| 35 | 33, 34 | bitrdi 287 |
. . . 4
⊢ (𝜑 → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀))) |
| 36 | 35 | anbi1d 631 |
. . 3
⊢ (𝜑 → ((𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵) ↔ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) ∧ ran 𝑐 ⊆ 𝐵))) |
| 37 | | an32 646 |
. . 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 𝑐 ⊆ 𝐵))) |