| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mapss2.b | . . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ 𝑊) | 
| 3 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) | 
| 4 |  | mapss 8930 | . . . 4
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) | 
| 5 | 2, 3, 4 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) | 
| 6 | 5 | ex 412 | . 2
⊢ (𝜑 → (𝐴 ⊆ 𝐵 → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))) | 
| 7 |  | mapss2.n | . . . . . 6
⊢ (𝜑 → 𝐶 ≠ ∅) | 
| 8 |  | n0 4352 | . . . . . 6
⊢ (𝐶 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐶) | 
| 9 | 7, 8 | sylib 218 | . . . . 5
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐶) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) → ∃𝑥 𝑥 ∈ 𝐶) | 
| 11 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑤 ∈ 𝐶 ↦ 𝑦) = (𝑤 ∈ 𝐶 ↦ 𝑦)) | 
| 12 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 = 𝑥) → 𝑦 = 𝑦) | 
| 13 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) | 
| 14 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 15 | 14 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑦 ∈ V) | 
| 16 | 11, 12, 13, 15 | fvmptd 7022 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥) = 𝑦) | 
| 17 | 16 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑦 = ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥)) | 
| 18 | 17 | ad4ant13 751 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → 𝑦 = ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥)) | 
| 19 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) | 
| 20 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ 𝐶) → 𝑦 ∈ 𝐴) | 
| 21 | 20 | fmpttd 7134 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐴) | 
| 22 |  | mapss2.a | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 ∈ 𝑉) | 
| 24 |  | mapss2.c | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈ 𝑍) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐶 ∈ 𝑍) | 
| 26 | 23, 25 | elmapd 8881 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐴 ↑m 𝐶) ↔ (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐴)) | 
| 27 | 21, 26 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐴 ↑m 𝐶)) | 
| 28 | 27 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐴 ↑m 𝐶)) | 
| 29 | 19, 28 | sseldd 3983 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐵 ↑m 𝐶)) | 
| 30 |  | elmapi 8890 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐶 ↦ 𝑦) ∈ (𝐵 ↑m 𝐶) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐵) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐵) | 
| 32 | 31 | adantlr 715 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → (𝑤 ∈ 𝐶 ↦ 𝑦):𝐶⟶𝐵) | 
| 33 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐶) | 
| 34 | 32, 33 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝐶 ↦ 𝑦)‘𝑥) ∈ 𝐵) | 
| 35 | 18, 34 | eqeltrd 2840 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵) | 
| 36 | 35 | ralrimiva 3145 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) → ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 37 |  | dfss3 3971 | . . . . . . 7
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 38 | 36, 37 | sylibr 234 | . . . . . 6
⊢ (((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐵) | 
| 39 | 38 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) → (𝑥 ∈ 𝐶 → 𝐴 ⊆ 𝐵)) | 
| 40 | 39 | exlimdv 1932 | . . . 4
⊢ ((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) → (∃𝑥 𝑥 ∈ 𝐶 → 𝐴 ⊆ 𝐵)) | 
| 41 | 10, 40 | mpd 15 | . . 3
⊢ ((𝜑 ∧ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) → 𝐴 ⊆ 𝐵) | 
| 42 | 41 | ex 412 | . 2
⊢ (𝜑 → ((𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶) → 𝐴 ⊆ 𝐵)) | 
| 43 | 6, 42 | impbid 212 | 1
⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))) |