Step | Hyp | Ref
| Expression |
1 | | difmap.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | difssd 4023 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) |
3 | | mapss 8499 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ (𝐴 ↑m 𝐶)) |
4 | 1, 2, 3 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ (𝐴 ↑m 𝐶)) |
5 | 4 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ (𝐴 ↑m 𝐶)) |
6 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) |
7 | 5, 6 | sseldd 3878 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → 𝑓 ∈ (𝐴 ↑m 𝐶)) |
8 | | difmap.n |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≠ ∅) |
9 | | n0 4235 |
. . . . . . . 8
⊢ (𝐶 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐶) |
10 | 8, 9 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐶) |
11 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → ∃𝑥 𝑥 ∈ 𝐶) |
12 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑓:𝐶⟶𝐵) → 𝑓:𝐶⟶𝐵) |
13 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑓:𝐶⟶𝐵) → 𝑥 ∈ 𝐶) |
14 | 12, 13 | ffvelrnd 6862 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑓:𝐶⟶𝐵) → (𝑓‘𝑥) ∈ 𝐵) |
15 | 14 | adantll 714 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑓:𝐶⟶𝐵) → (𝑓‘𝑥) ∈ 𝐵) |
16 | | elmapi 8459 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶) → 𝑓:𝐶⟶(𝐴 ∖ 𝐵)) |
17 | 16 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶) ∧ 𝑥 ∈ 𝐶) → 𝑓:𝐶⟶(𝐴 ∖ 𝐵)) |
18 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
19 | 17, 18 | ffvelrnd 6862 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶) ∧ 𝑥 ∈ 𝐶) → (𝑓‘𝑥) ∈ (𝐴 ∖ 𝐵)) |
20 | | eldifn 4018 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ∈ (𝐴 ∖ 𝐵) → ¬ (𝑓‘𝑥) ∈ 𝐵) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶) ∧ 𝑥 ∈ 𝐶) → ¬ (𝑓‘𝑥) ∈ 𝐵) |
22 | 21 | ad4ant23 753 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑓:𝐶⟶𝐵) → ¬ (𝑓‘𝑥) ∈ 𝐵) |
23 | 15, 22 | pm2.65da 817 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) → ¬ 𝑓:𝐶⟶𝐵) |
24 | 23 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → (𝑥 ∈ 𝐶 → ¬ 𝑓:𝐶⟶𝐵)) |
25 | 24 | exlimdv 1940 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → (∃𝑥 𝑥 ∈ 𝐶 → ¬ 𝑓:𝐶⟶𝐵)) |
26 | 11, 25 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → ¬ 𝑓:𝐶⟶𝐵) |
27 | | difmap.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
28 | | difmap.v |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑍) |
29 | | elmapg 8450 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑍) → (𝑓 ∈ (𝐵 ↑m 𝐶) ↔ 𝑓:𝐶⟶𝐵)) |
30 | 27, 28, 29 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m 𝐶) ↔ 𝑓:𝐶⟶𝐵)) |
31 | 30 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → (𝑓 ∈ (𝐵 ↑m 𝐶) ↔ 𝑓:𝐶⟶𝐵)) |
32 | 26, 31 | mtbird 328 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → ¬ 𝑓 ∈ (𝐵 ↑m 𝐶)) |
33 | 7, 32 | eldifd 3854 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)) → 𝑓 ∈ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶))) |
34 | 33 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)𝑓 ∈ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶))) |
35 | | dfss3 3865 |
. 2
⊢ (((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶)) ↔ ∀𝑓 ∈ ((𝐴 ∖ 𝐵) ↑m 𝐶)𝑓 ∈ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶))) |
36 | 34, 35 | sylibr 237 |
1
⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶))) |