Step | Hyp | Ref
| Expression |
1 | | mapss2.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ 𝑊) |
3 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) |
4 | | mapss 7786 |
. . . 4
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
5 | 2, 3, 4 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
6 | 5 | ex 449 |
. 2
⊢ (𝜑 → (𝐴 ⊆ 𝐵 → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))) |
7 | | mapss2.n |
. . . . . 6
⊢ (𝜑 → 𝐶 ≠ ∅) |
8 | | n0 3890 |
. . . . . 6
⊢ (𝐶 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐶) |
9 | 7, 8 | sylib 207 |
. . . . 5
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐶) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) → ∃𝑥 𝑥 ∈ 𝐶) |
11 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑤 ∈ 𝐶 ↦ 𝑦) = (𝑤 ∈ 𝐶 ↦ 𝑦)) |
12 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 = 𝑥) → 𝑦 = 𝑦) |
13 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
14 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑦 ∈ V) |
16 | 11, 12, 13, 15 | fvmptd 6197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥) = 𝑦) |
17 | 16 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑦 = ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥)) |
18 | 17 | ad4ant13 1284 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → 𝑦 = ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥)) |
19 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
20 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ 𝐶) → 𝑦 ∈ 𝐴) |
21 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝐶 ↦ 𝑦) = (𝑤 ∈ 𝐶 ↦ 𝑦) |
22 | 20, 21 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐴) |
23 | | mapss2.a |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 ∈ 𝑉) |
25 | | mapss2.c |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈ 𝑍) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐶 ∈ 𝑍) |
27 | 24, 26 | elmapd 7758 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐴 ↑𝑚 𝐶) ↔ (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐴)) |
28 | 22, 27 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐴 ↑𝑚 𝐶)) |
29 | 28 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐴 ↑𝑚 𝐶)) |
30 | 19, 29 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐵 ↑𝑚 𝐶)) |
31 | | elmapi 7765 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐵 ↑𝑚 𝐶) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐵) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐵) |
33 | 32 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐵) |
34 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐶) |
35 | 33, 34 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥) ∈ 𝐵) |
36 | 18, 35 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
37 | 36 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) → ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝐵) |
38 | | dfss3 3558 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝐵) |
39 | 37, 38 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐵) |
40 | 39 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) → (𝑥 ∈ 𝐶 → 𝐴 ⊆ 𝐵)) |
41 | 40 | exlimdv 1848 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) → (∃𝑥 𝑥 ∈ 𝐶 → 𝐴 ⊆ 𝐵)) |
42 | 10, 41 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) → 𝐴 ⊆ 𝐵) |
43 | 42 | ex 449 |
. 2
⊢ (𝜑 → ((𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶) → 𝐴 ⊆ 𝐵)) |
44 | 6, 43 | impbid 201 |
1
⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))) |