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 6558 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩}) |
6 | | funtp.3 |
. . . . . 6
⊢ 𝐶 ∈ V |
7 | | funtp.6 |
. . . . . 6
⊢ 𝐹 ∈ V |
8 | 6, 7 | funsn 6555 |
. . . . 5
⊢ Fun
{⟨𝐶, 𝐹⟩} |
9 | 5, 8 | jctir 522 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → (Fun {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∧ Fun {⟨𝐶, 𝐹⟩})) |
10 | 3, 4 | dmprop 6170 |
. . . . . . 7
⊢ dom
{⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} = {𝐴, 𝐵} |
11 | | df-pr 4590 |
. . . . . . 7
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
12 | 10, 11 | eqtri 2761 |
. . . . . 6
⊢ dom
{⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} = ({𝐴} ∪ {𝐵}) |
13 | 7 | dmsnop 6169 |
. . . . . 6
⊢ dom
{⟨𝐶, 𝐹⟩} = {𝐶} |
14 | 12, 13 | ineq12i 4171 |
. . . . 5
⊢ (dom
{⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∩ dom {⟨𝐶, 𝐹⟩}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶}) |
15 | | disjsn2 4674 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐶 → ({𝐴} ∩ {𝐶}) = ∅) |
16 | | disjsn2 4674 |
. . . . . . 7
⊢ (𝐵 ≠ 𝐶 → ({𝐵} ∩ {𝐶}) = ∅) |
17 | 15, 16 | anim12i 614 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
18 | | undisj1 4422 |
. . . . . 6
⊢ ((({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅) ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
19 | 17, 18 | sylib 217 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
20 | 14, 19 | eqtrid 2785 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (dom {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∩ dom {⟨𝐶, 𝐹⟩}) = ∅) |
21 | | funun 6548 |
. . . 4
⊢ (((Fun
{⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∧ Fun {⟨𝐶, 𝐹⟩}) ∧ (dom {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∩ dom {⟨𝐶, 𝐹⟩}) = ∅) → Fun ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∪ {⟨𝐶, 𝐹⟩})) |
22 | 9, 20, 21 | syl2an 597 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∪ {⟨𝐶, 𝐹⟩})) |
23 | 22 | 3impb 1116 |
. 2
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∪ {⟨𝐶, 𝐹⟩})) |
24 | | df-tp 4592 |
. . 3
⊢
{⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} = ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∪ {⟨𝐶, 𝐹⟩}) |
25 | 24 | funeqi 6523 |
. 2
⊢ (Fun
{⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} ↔ Fun ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩} ∪ {⟨𝐶, 𝐹⟩})) |
26 | 23, 25 | sylibr 233 |
1
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}) |