Proof of Theorem mapprop
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) → 𝑋 ∈ 𝑉) |
2 | | simpl 472 |
. . . . . . 7
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) → 𝑌 ∈ 𝑉) |
3 | 1, 2 | anim12i 588 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) |
4 | 3 | 3adant3 1074 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) |
5 | | simpr 476 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) → 𝐴 ∈ 𝑅) |
6 | | simpr 476 |
. . . . . . 7
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) → 𝐵 ∈ 𝑅) |
7 | 5, 6 | anim12i 588 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅)) → (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅)) |
8 | 7 | 3adant3 1074 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅)) |
9 | | simpl 472 |
. . . . . 6
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊) → 𝑋 ≠ 𝑌) |
10 | 9 | 3ad2ant3 1077 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝑋 ≠ 𝑌) |
11 | | fprg 6327 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) ∧ 𝑋 ≠ 𝑌) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}:{𝑋, 𝑌}⟶{𝐴, 𝐵}) |
12 | 4, 8, 10, 11 | syl3anc 1318 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}:{𝑋, 𝑌}⟶{𝐴, 𝐵}) |
13 | | mapprop.f |
. . . . 5
⊢ 𝐹 = {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} |
14 | 13 | feq1i 5949 |
. . . 4
⊢ (𝐹:{𝑋, 𝑌}⟶{𝐴, 𝐵} ↔ {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}:{𝑋, 𝑌}⟶{𝐴, 𝐵}) |
15 | 12, 14 | sylibr 223 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹:{𝑋, 𝑌}⟶{𝐴, 𝐵}) |
16 | | prssi 4293 |
. . . . 5
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → {𝐴, 𝐵} ⊆ 𝑅) |
17 | 7, 16 | syl 17 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅)) → {𝐴, 𝐵} ⊆ 𝑅) |
18 | 17 | 3adant3 1074 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → {𝐴, 𝐵} ⊆ 𝑅) |
19 | 15, 18 | fssd 5970 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹:{𝑋, 𝑌}⟶𝑅) |
20 | | simpr 476 |
. . . 4
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊) → 𝑅 ∈ 𝑊) |
21 | 20 | 3ad2ant3 1077 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝑅 ∈ 𝑊) |
22 | | prex 4836 |
. . 3
⊢ {𝑋, 𝑌} ∈ V |
23 | | elmapg 7757 |
. . 3
⊢ ((𝑅 ∈ 𝑊 ∧ {𝑋, 𝑌} ∈ V) → (𝐹 ∈ (𝑅 ↑𝑚 {𝑋, 𝑌}) ↔ 𝐹:{𝑋, 𝑌}⟶𝑅)) |
24 | 21, 22, 23 | sylancl 693 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → (𝐹 ∈ (𝑅 ↑𝑚 {𝑋, 𝑌}) ↔ 𝐹:{𝑋, 𝑌}⟶𝑅)) |
25 | 19, 24 | mpbird 246 |
1
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹 ∈ (𝑅 ↑𝑚 {𝑋, 𝑌})) |