Proof of Theorem funtpg
Step | Hyp | Ref
| Expression |
1 | | 3simpa 900 |
. . . 4
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉)) |
2 | | 3simpa 900 |
. . . 4
⊢
((A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (A ∈ 𝐹 ∧ B ∈ 𝐺)) |
3 | | simp1 903 |
. . . 4
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → 𝑋 ≠ 𝑌) |
4 | | funprg 4892 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺) ∧ 𝑋 ≠ 𝑌) → Fun {〈𝑋, A〉, 〈𝑌, B〉}) |
5 | 1, 2, 3, 4 | syl3an 1176 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, A〉, 〈𝑌, B〉}) |
6 | | simp13 935 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → 𝑍 ∈ 𝑊) |
7 | | simp23 938 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → 𝐶 ∈ 𝐻) |
8 | | funsng 4889 |
. . . 4
⊢ ((𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻) → Fun {〈𝑍, 𝐶〉}) |
9 | 6, 7, 8 | syl2anc 391 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑍, 𝐶〉}) |
10 | 2 | 3ad2ant2 925 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (A ∈ 𝐹 ∧ B ∈ 𝐺)) |
11 | | dmpropg 4736 |
. . . . . 6
⊢
((A ∈ 𝐹 ∧ B ∈ 𝐺) → dom {〈𝑋, A〉, 〈𝑌, B〉} = {𝑋, 𝑌}) |
12 | 10, 11 | syl 14 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, A〉, 〈𝑌, B〉} = {𝑋, 𝑌}) |
13 | | dmsnopg 4735 |
. . . . . 6
⊢ (𝐶 ∈ 𝐻 → dom {〈𝑍, 𝐶〉} = {𝑍}) |
14 | 7, 13 | syl 14 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
15 | 12, 14 | ineq12d 3133 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, A〉, 〈𝑌, B〉} ∩ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∩ {𝑍})) |
16 | | elpri 3387 |
. . . . . . . 8
⊢ (𝑍 ∈ {𝑋, 𝑌} → (𝑍 = 𝑋 ∨ 𝑍 = 𝑌)) |
17 | | nner 2207 |
. . . . . . . . . . . 12
⊢ (𝑋 = 𝑍 → ¬ 𝑋 ≠ 𝑍) |
18 | 17 | eqcoms 2040 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑋 → ¬ 𝑋 ≠ 𝑍) |
19 | | 3mix2 1073 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ≠ 𝑍 → (¬ 𝑋 ≠ 𝑌 ∨ ¬
𝑋 ≠ 𝑍 ∨ ¬
𝑌 ≠ 𝑍)) |
20 | 18, 19 | syl 14 |
. . . . . . . . . 10
⊢ (𝑍 = 𝑋 → (¬ 𝑋 ≠ 𝑌 ∨ ¬
𝑋 ≠ 𝑍 ∨ ¬
𝑌 ≠ 𝑍)) |
21 | | nner 2207 |
. . . . . . . . . . . 12
⊢ (𝑌 = 𝑍 → ¬ 𝑌 ≠ 𝑍) |
22 | 21 | eqcoms 2040 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑌 → ¬ 𝑌 ≠ 𝑍) |
23 | | 3mix3 1074 |
. . . . . . . . . . 11
⊢ (¬
𝑌 ≠ 𝑍 → (¬ 𝑋 ≠ 𝑌 ∨ ¬
𝑋 ≠ 𝑍 ∨ ¬
𝑌 ≠ 𝑍)) |
24 | 22, 23 | syl 14 |
. . . . . . . . . 10
⊢ (𝑍 = 𝑌 → (¬ 𝑋 ≠ 𝑌 ∨ ¬
𝑋 ≠ 𝑍 ∨ ¬
𝑌 ≠ 𝑍)) |
25 | 20, 24 | jaoi 635 |
. . . . . . . . 9
⊢ ((𝑍 = 𝑋 ∨ 𝑍 = 𝑌) → (¬ 𝑋 ≠ 𝑌 ∨ ¬
𝑋 ≠ 𝑍 ∨ ¬
𝑌 ≠ 𝑍)) |
26 | | 3ianorr 1203 |
. . . . . . . . 9
⊢ ((¬
𝑋 ≠ 𝑌 ∨ ¬
𝑋 ≠ 𝑍 ∨ ¬
𝑌 ≠ 𝑍) → ¬ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
27 | 25, 26 | syl 14 |
. . . . . . . 8
⊢ ((𝑍 = 𝑋 ∨ 𝑍 = 𝑌) → ¬ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
28 | 16, 27 | syl 14 |
. . . . . . 7
⊢ (𝑍 ∈ {𝑋, 𝑌} → ¬ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
29 | 28 | con2i 557 |
. . . . . 6
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ¬ 𝑍 ∈ {𝑋, 𝑌}) |
30 | | disjsn 3423 |
. . . . . 6
⊢ (({𝑋, 𝑌} ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ {𝑋, 𝑌}) |
31 | 29, 30 | sylibr 137 |
. . . . 5
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) |
32 | 31 | 3ad2ant3 926 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) |
33 | 15, 32 | eqtrd 2069 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, A〉, 〈𝑌, B〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) |
34 | | funun 4887 |
. . 3
⊢ (((Fun
{〈𝑋, A〉, 〈𝑌, B〉} ∧ Fun
{〈𝑍, 𝐶〉}) ∧
(dom {〈𝑋, A〉, 〈𝑌, B〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) → Fun ({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉})) |
35 | 5, 9, 33, 34 | syl21anc 1133 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun ({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉})) |
36 | | df-tp 3375 |
. . 3
⊢
{〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} = ({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉}) |
37 | 36 | funeqi 4865 |
. 2
⊢ (Fun
{〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} ↔ Fun ({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉})) |
38 | 35, 37 | sylibr 137 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉}) |