Proof of Theorem mapvalg
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | mapex 3261 |
. . 3
⊢ ((B
∈ D ∧ A ∈ C)
→ {f∣f:B–→A}
∈ V) |
| 2 | 1 | ancoms 334 |
. 2
⊢ ((A
∈ C ∧ B ∈ D)
→ {f∣f:B–→A}
∈ V) |
| 3 | | feq3 2750 |
. . . . . . 7
⊢ (x =
A → (f:y–→x
↔ f:y–→A)) |
| 4 | 3 | biabdv 1183 |
. . . . . 6
⊢ (x =
A → {f∣f:y–→x}
= {f∣f:y–→A}) |
| 5 | | feq2 2749 |
. . . . . . 7
⊢ (y =
B → (f:y–→A
↔ f:B–→A)) |
| 6 | 5 | biabdv 1183 |
. . . . . 6
⊢ (y =
B → {f∣f:y–→A}
= {f∣f:B–→A}) |
| 7 | | df-map 3259 |
. . . . . . 7
⊢ ↑m =
{⟨⟨x, y⟩, z⟩∣z
= {f∣f:y–→x}} |
| 8 | | visset 1350 |
. . . . . . . . . 10
⊢ x
∈ V |
| 9 | | visset 1350 |
. . . . . . . . . 10
⊢ y
∈ V |
| 10 | 8, 9 | pm3.2i 234 |
. . . . . . . . 9
⊢ (x
∈ V ∧ y ∈
V) |
| 11 | 10 | biantrur 544 |
. . . . . . . 8
⊢ (z =
{f∣f:y–→x}
↔ ((x ∈ V ∧ y ∈ V) ∧ z = {f∣f:y–→x})) |
| 12 | 11 | bioprabi 3027 |
. . . . . . 7
⊢ {⟨⟨x, y⟩,
z⟩∣z = {f∣f:y–→x}} = {⟨⟨x, y⟩,
z⟩∣((x ∈ V ∧ y ∈ V) ∧ z = {f∣f:y–→x})} |
| 13 | 7, 12 | eqtr 1119 |
. . . . . 6
⊢ ↑m =
{⟨⟨x, y⟩, z⟩∣((x ∈ V ∧ y ∈ V) ∧ z = {f∣f:y–→x})} |
| 14 | 4, 6, 13 | oprabval2g 3050 |
. . . . 5
⊢ ((A
∈ V ∧ B ∈ V
∧ {f∣f:B–→A}
∈ V) → (A
↑m B) = {f∣f:B–→A}) |
| 15 | 14 | 3exp 611 |
. . . 4
⊢ (A
∈ V → (B ∈ V
→ ({f∣f:B–→A}
∈ V → (A
↑m B) = {f∣f:B–→A}))) |
| 16 | 15 | imp 277 |
. . 3
⊢ ((A
∈ V ∧ B ∈ V)
→ ({f∣f:B–→A}
∈ V → (A
↑m B) = {f∣f:B–→A})) |
| 17 | | elisset 1354 |
. . 3
⊢ (A
∈ C → A ∈ V) |
| 18 | | elisset 1354 |
. . 3
⊢ (B
∈ D → B ∈ V) |
| 19 | 16, 17, 18 | syl2an 349 |
. 2
⊢ ((A
∈ C ∧ B ∈ D)
→ ({f∣f:B–→A}
∈ V → (A
↑m B) = {f∣f:B–→A})) |
| 20 | 2, 19 | mpd 46 |
1
⊢ ((A
∈ C ∧ B ∈ D)
→ (A ↑m
B) = {f∣f:B–→A}) |
Home