Proof of Theorem fntpg
Step | Hyp | Ref
| Expression |
1 | | funtpg 4893 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉}) |
2 | | dmsnopg 4735 |
. . . . . . . . . 10
⊢ (A ∈ 𝐹 → dom {〈𝑋, A〉} = {𝑋}) |
3 | 2 | 3ad2ant1 924 |
. . . . . . . . 9
⊢
((A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑋, A〉} = {𝑋}) |
4 | | dmsnopg 4735 |
. . . . . . . . . 10
⊢ (B ∈ 𝐺 → dom {〈𝑌, B〉} = {𝑌}) |
5 | 4 | 3ad2ant2 925 |
. . . . . . . . 9
⊢
((A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑌, B〉} = {𝑌}) |
6 | 3, 5 | jca 290 |
. . . . . . . 8
⊢
((A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (dom {〈𝑋, A〉} = {𝑋} ∧ dom
{〈𝑌, B〉} = {𝑌})) |
7 | 6 | 3ad2ant2 925 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, A〉} = {𝑋} ∧ dom
{〈𝑌, B〉} = {𝑌})) |
8 | | uneq12 3086 |
. . . . . . 7
⊢ ((dom
{〈𝑋, A〉} = {𝑋} ∧ dom
{〈𝑌, B〉} = {𝑌}) → (dom {〈𝑋, A〉} ∪ dom {〈𝑌, B〉}) = ({𝑋} ∪ {𝑌})) |
9 | 7, 8 | syl 14 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, A〉} ∪ dom {〈𝑌, B〉}) = ({𝑋} ∪ {𝑌})) |
10 | | df-pr 3374 |
. . . . . 6
⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌}) |
11 | 9, 10 | syl6eqr 2087 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, A〉} ∪ dom {〈𝑌, B〉}) = {𝑋, 𝑌}) |
12 | | df-pr 3374 |
. . . . . . . 8
⊢
{〈𝑋, A〉, 〈𝑌, B〉} = ({〈𝑋, A〉} ∪ {〈𝑌, B〉}) |
13 | 12 | dmeqi 4479 |
. . . . . . 7
⊢ dom
{〈𝑋, A〉, 〈𝑌, B〉} = dom ({〈𝑋, A〉} ∪ {〈𝑌, B〉}) |
14 | 13 | eqeq1i 2044 |
. . . . . 6
⊢ (dom
{〈𝑋, A〉, 〈𝑌, B〉} = {𝑋, 𝑌} ↔ dom ({〈𝑋, A〉} ∪ {〈𝑌, B〉}) = {𝑋, 𝑌}) |
15 | | dmun 4485 |
. . . . . . 7
⊢ dom
({〈𝑋, A〉} ∪ {〈𝑌, B〉}) = (dom {〈𝑋, A〉} ∪ dom {〈𝑌, B〉}) |
16 | 15 | eqeq1i 2044 |
. . . . . 6
⊢ (dom
({〈𝑋, A〉} ∪ {〈𝑌, B〉}) = {𝑋, 𝑌} ↔ (dom {〈𝑋, A〉} ∪ dom {〈𝑌, B〉}) = {𝑋, 𝑌}) |
17 | 14, 16 | bitri 173 |
. . . . 5
⊢ (dom
{〈𝑋, A〉, 〈𝑌, B〉} = {𝑋, 𝑌} ↔ (dom {〈𝑋, A〉} ∪ dom {〈𝑌, B〉}) = {𝑋, 𝑌}) |
18 | 11, 17 | sylibr 137 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, A〉, 〈𝑌, B〉} = {𝑋, 𝑌}) |
19 | | dmsnopg 4735 |
. . . . . 6
⊢ (𝐶 ∈ 𝐻 → dom {〈𝑍, 𝐶〉} = {𝑍}) |
20 | 19 | 3ad2ant3 926 |
. . . . 5
⊢
((A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
21 | 20 | 3ad2ant2 925 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
22 | 18, 21 | uneq12d 3092 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, A〉, 〈𝑌, B〉} ∪ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∪ {𝑍})) |
23 | | df-tp 3375 |
. . . . 5
⊢
{〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} = ({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉}) |
24 | 23 | dmeqi 4479 |
. . . 4
⊢ dom
{〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} = dom ({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉}) |
25 | | dmun 4485 |
. . . 4
⊢ dom
({〈𝑋, A〉, 〈𝑌, B〉} ∪ {〈𝑍, 𝐶〉}) = (dom {〈𝑋, A〉, 〈𝑌, B〉} ∪ dom {〈𝑍, 𝐶〉}) |
26 | 24, 25 | eqtri 2057 |
. . 3
⊢ dom
{〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} = (dom {〈𝑋, A〉, 〈𝑌, B〉} ∪ dom {〈𝑍, 𝐶〉}) |
27 | | df-tp 3375 |
. . 3
⊢ {𝑋, 𝑌, 𝑍} = ({𝑋, 𝑌} ∪ {𝑍}) |
28 | 22, 26, 27 | 3eqtr4g 2094 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} = {𝑋, 𝑌, 𝑍}) |
29 | | df-fn 4848 |
. 2
⊢
({〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍} ↔ (Fun {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} ∧
dom {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} = {𝑋, 𝑌, 𝑍})) |
30 | 1, 28, 29 | sylanbrc 394 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧
(A ∈
𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍}) |