Proof of Theorem fntpg
Step | Hyp | Ref
| Expression |
1 | | funtpg 6435 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}) |
2 | | dmsnopg 6076 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐹 → dom {〈𝑋, 𝐴〉} = {𝑋}) |
3 | 2 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑋, 𝐴〉} = {𝑋}) |
4 | | dmsnopg 6076 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝐺 → dom {〈𝑌, 𝐵〉} = {𝑌}) |
5 | 4 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑌, 𝐵〉} = {𝑌}) |
6 | 3, 5 | jca 515 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (dom {〈𝑋, 𝐴〉} = {𝑋} ∧ dom {〈𝑌, 𝐵〉} = {𝑌})) |
7 | 6 | 3ad2ant2 1136 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉} = {𝑋} ∧ dom {〈𝑌, 𝐵〉} = {𝑌})) |
8 | | uneq12 4072 |
. . . . . . 7
⊢ ((dom
{〈𝑋, 𝐴〉} = {𝑋} ∧ dom {〈𝑌, 𝐵〉} = {𝑌}) → (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = ({𝑋} ∪ {𝑌})) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = ({𝑋} ∪ {𝑌})) |
10 | | df-pr 4544 |
. . . . . 6
⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌}) |
11 | 9, 10 | eqtr4di 2796 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
12 | | df-pr 4544 |
. . . . . . . 8
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = ({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) |
13 | 12 | dmeqi 5773 |
. . . . . . 7
⊢ dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = dom ({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) |
14 | 13 | eqeq1i 2742 |
. . . . . 6
⊢ (dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌} ↔ dom ({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
15 | | dmun 5779 |
. . . . . . 7
⊢ dom
({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) = (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) |
16 | 15 | eqeq1i 2742 |
. . . . . 6
⊢ (dom
({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) = {𝑋, 𝑌} ↔ (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
17 | 14, 16 | bitri 278 |
. . . . 5
⊢ (dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌} ↔ (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
18 | 11, 17 | sylibr 237 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌}) |
19 | | dmsnopg 6076 |
. . . . . 6
⊢ (𝐶 ∈ 𝐻 → dom {〈𝑍, 𝐶〉} = {𝑍}) |
20 | 19 | 3ad2ant3 1137 |
. . . . 5
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
21 | 20 | 3ad2ant2 1136 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
22 | 18, 21 | uneq12d 4078 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∪ {𝑍})) |
23 | | df-tp 4546 |
. . . . 5
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) |
24 | 23 | dmeqi 5773 |
. . . 4
⊢ dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = dom ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) |
25 | | dmun 5779 |
. . . 4
⊢ dom
({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) = (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ dom {〈𝑍, 𝐶〉}) |
26 | 24, 25 | eqtri 2765 |
. . 3
⊢ dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ dom {〈𝑍, 𝐶〉}) |
27 | | df-tp 4546 |
. . 3
⊢ {𝑋, 𝑌, 𝑍} = ({𝑋, 𝑌} ∪ {𝑍}) |
28 | 22, 26, 27 | 3eqtr4g 2803 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = {𝑋, 𝑌, 𝑍}) |
29 | | df-fn 6383 |
. 2
⊢
({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍} ↔ (Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} ∧ dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = {𝑋, 𝑌, 𝑍})) |
30 | 1, 28, 29 | sylanbrc 586 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍}) |