Proof of Theorem funtpg
Step | Hyp | Ref
| Expression |
1 | | 3simpa 989 |
. . . 4
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉)) |
2 | | 3simpa 989 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺)) |
3 | | simp1 992 |
. . . 4
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → 𝑋 ≠ 𝑌) |
4 | | funprg 5248 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺) ∧ 𝑋 ≠ 𝑌) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}) |
5 | 1, 2, 3, 4 | syl3an 1275 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}) |
6 | | simp13 1024 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → 𝑍 ∈ 𝑊) |
7 | | simp23 1027 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → 𝐶 ∈ 𝐻) |
8 | | funsng 5244 |
. . . 4
⊢ ((𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻) → Fun {〈𝑍, 𝐶〉}) |
9 | 6, 7, 8 | syl2anc 409 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑍, 𝐶〉}) |
10 | 2 | 3ad2ant2 1014 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺)) |
11 | | dmpropg 5083 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌}) |
12 | 10, 11 | syl 14 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌}) |
13 | | dmsnopg 5082 |
. . . . . 6
⊢ (𝐶 ∈ 𝐻 → dom {〈𝑍, 𝐶〉} = {𝑍}) |
14 | 7, 13 | syl 14 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
15 | 12, 14 | ineq12d 3329 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∩ {𝑍})) |
16 | | elpri 3606 |
. . . . . . . 8
⊢ (𝑍 ∈ {𝑋, 𝑌} → (𝑍 = 𝑋 ∨ 𝑍 = 𝑌)) |
17 | | nner 2344 |
. . . . . . . . . . . 12
⊢ (𝑋 = 𝑍 → ¬ 𝑋 ≠ 𝑍) |
18 | 17 | eqcoms 2173 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑋 → ¬ 𝑋 ≠ 𝑍) |
19 | | 3mix2 1162 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ≠ 𝑍 → (¬ 𝑋 ≠ 𝑌 ∨ ¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
20 | 18, 19 | syl 14 |
. . . . . . . . . 10
⊢ (𝑍 = 𝑋 → (¬ 𝑋 ≠ 𝑌 ∨ ¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
21 | | nner 2344 |
. . . . . . . . . . . 12
⊢ (𝑌 = 𝑍 → ¬ 𝑌 ≠ 𝑍) |
22 | 21 | eqcoms 2173 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑌 → ¬ 𝑌 ≠ 𝑍) |
23 | | 3mix3 1163 |
. . . . . . . . . . 11
⊢ (¬
𝑌 ≠ 𝑍 → (¬ 𝑋 ≠ 𝑌 ∨ ¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
24 | 22, 23 | syl 14 |
. . . . . . . . . 10
⊢ (𝑍 = 𝑌 → (¬ 𝑋 ≠ 𝑌 ∨ ¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
25 | 20, 24 | jaoi 711 |
. . . . . . . . 9
⊢ ((𝑍 = 𝑋 ∨ 𝑍 = 𝑌) → (¬ 𝑋 ≠ 𝑌 ∨ ¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
26 | | 3ianorr 1304 |
. . . . . . . . 9
⊢ ((¬
𝑋 ≠ 𝑌 ∨ ¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍) → ¬ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
27 | 25, 26 | syl 14 |
. . . . . . . 8
⊢ ((𝑍 = 𝑋 ∨ 𝑍 = 𝑌) → ¬ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
28 | 16, 27 | syl 14 |
. . . . . . 7
⊢ (𝑍 ∈ {𝑋, 𝑌} → ¬ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
29 | 28 | con2i 622 |
. . . . . 6
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ¬ 𝑍 ∈ {𝑋, 𝑌}) |
30 | | disjsn 3645 |
. . . . . 6
⊢ (({𝑋, 𝑌} ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ {𝑋, 𝑌}) |
31 | 29, 30 | sylibr 133 |
. . . . 5
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) |
32 | 31 | 3ad2ant3 1015 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) |
33 | 15, 32 | eqtrd 2203 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) |
34 | | funun 5242 |
. . 3
⊢ (((Fun
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∧ Fun {〈𝑍, 𝐶〉}) ∧ (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) → Fun ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉})) |
35 | 5, 9, 33, 34 | syl21anc 1232 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉})) |
36 | | df-tp 3591 |
. . 3
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) |
37 | 36 | funeqi 5219 |
. 2
⊢ (Fun
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} ↔ Fun ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉})) |
38 | 35, 37 | sylibr 133 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}) |