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 6436 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉}) |
6 | | funtp.3 |
. . . . . 6
⊢ 𝐶 ∈ V |
7 | | funtp.6 |
. . . . . 6
⊢ 𝐹 ∈ V |
8 | 6, 7 | funsn 6433 |
. . . . 5
⊢ Fun
{〈𝐶, 𝐹〉} |
9 | 5, 8 | jctir 524 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → (Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∧ Fun {〈𝐶, 𝐹〉})) |
10 | 3, 4 | dmprop 6080 |
. . . . . . 7
⊢ dom
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} = {𝐴, 𝐵} |
11 | | df-pr 4544 |
. . . . . . 7
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
12 | 10, 11 | eqtri 2765 |
. . . . . 6
⊢ dom
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} = ({𝐴} ∪ {𝐵}) |
13 | 7 | dmsnop 6079 |
. . . . . 6
⊢ dom
{〈𝐶, 𝐹〉} = {𝐶} |
14 | 12, 13 | ineq12i 4125 |
. . . . 5
⊢ (dom
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∩ dom {〈𝐶, 𝐹〉}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶}) |
15 | | disjsn2 4628 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐶 → ({𝐴} ∩ {𝐶}) = ∅) |
16 | | disjsn2 4628 |
. . . . . . 7
⊢ (𝐵 ≠ 𝐶 → ({𝐵} ∩ {𝐶}) = ∅) |
17 | 15, 16 | anim12i 616 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
18 | | undisj1 4376 |
. . . . . 6
⊢ ((({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅) ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
19 | 17, 18 | sylib 221 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
20 | 14, 19 | eqtrid 2789 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (dom {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∩ dom {〈𝐶, 𝐹〉}) = ∅) |
21 | | funun 6426 |
. . . 4
⊢ (((Fun
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∧ Fun {〈𝐶, 𝐹〉}) ∧ (dom {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∩ dom {〈𝐶, 𝐹〉}) = ∅) → Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
22 | 9, 20, 21 | syl2an 599 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
23 | 22 | 3impb 1117 |
. 2
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
24 | | df-tp 4546 |
. . 3
⊢
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} = ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉}) |
25 | 24 | funeqi 6401 |
. 2
⊢ (Fun
{〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} ↔ Fun ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉} ∪ {〈𝐶, 𝐹〉})) |
26 | 23, 25 | sylibr 237 |
1
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) |