Proof of Theorem funtp
| Step | Hyp | Ref
| Expression |
| 1 | | funtp.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 2 | | funtp.2 |
. . . . . 6
⊢ 𝐵 ∈ V |
| 3 | | funtp.4 |
. . . . . 6
⊢ 𝐷 ∈ V |
| 4 | | funtp.5 |
. . . . . 6
⊢ 𝐸 ∈ V |
| 5 | 1, 2, 3, 4 | funpr 6622 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉}) |
| 6 | | funtp.3 |
. . . . . 6
⊢ 𝐶 ∈ V |
| 7 | | funtp.6 |
. . . . . 6
⊢ 𝐹 ∈ V |
| 8 | 6, 7 | funsn 6619 |
. . . . 5
⊢ Fun
{〈𝐶, 𝐹〉} |
| 9 | 5, 8 | jctir 520 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → (Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∧ Fun {〈𝐶, 𝐹〉})) |
| 10 | 3, 4 | dmprop 6237 |
. . . . . . 7
⊢ dom
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} = {𝐴, 𝐵} |
| 11 | | df-pr 4629 |
. . . . . . 7
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
| 12 | 10, 11 | eqtri 2765 |
. . . . . 6
⊢ dom
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} = ({𝐴} ∪ {𝐵}) |
| 13 | 7 | dmsnop 6236 |
. . . . . 6
⊢ dom
{〈𝐶, 𝐹〉} = {𝐶} |
| 14 | 12, 13 | ineq12i 4218 |
. . . . 5
⊢ (dom
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∩ dom {〈𝐶, 𝐹〉}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶}) |
| 15 | | disjsn2 4712 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐶 → ({𝐴} ∩ {𝐶}) = ∅) |
| 16 | | disjsn2 4712 |
. . . . . . 7
⊢ (𝐵 ≠ 𝐶 → ({𝐵} ∩ {𝐶}) = ∅) |
| 17 | 15, 16 | anim12i 613 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
| 18 | | undisj1 4462 |
. . . . . 6
⊢ ((({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅) ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
| 19 | 17, 18 | sylib 218 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
| 20 | 14, 19 | eqtrid 2789 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (dom {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∩ dom {〈𝐶, 𝐹〉}) = ∅) |
| 21 | | funun 6612 |
. . . 4
⊢ (((Fun
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∧ Fun {〈𝐶, 𝐹〉}) ∧ (dom {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∩ dom {〈𝐶, 𝐹〉}) = ∅) → Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
| 22 | 9, 20, 21 | syl2an 596 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
| 23 | 22 | 3impb 1115 |
. 2
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
| 24 | | df-tp 4631 |
. . 3
⊢
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} = ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉}) |
| 25 | 24 | funeqi 6587 |
. 2
⊢ (Fun
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} ↔ Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
| 26 | 23, 25 | sylibr 234 |
1
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) |