Proof of Theorem fntpg
| Step | Hyp | Ref
| Expression |
| 1 | | funtpg 6621 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}) |
| 2 | | dmsnopg 6233 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐹 → dom {〈𝑋, 𝐴〉} = {𝑋}) |
| 3 | 2 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑋, 𝐴〉} = {𝑋}) |
| 4 | | dmsnopg 6233 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝐺 → dom {〈𝑌, 𝐵〉} = {𝑌}) |
| 5 | 4 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑌, 𝐵〉} = {𝑌}) |
| 6 | 3, 5 | jca 511 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (dom {〈𝑋, 𝐴〉} = {𝑋} ∧ dom {〈𝑌, 𝐵〉} = {𝑌})) |
| 7 | 6 | 3ad2ant2 1135 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉} = {𝑋} ∧ dom {〈𝑌, 𝐵〉} = {𝑌})) |
| 8 | | uneq12 4163 |
. . . . . . 7
⊢ ((dom
{〈𝑋, 𝐴〉} = {𝑋} ∧ dom {〈𝑌, 𝐵〉} = {𝑌}) → (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = ({𝑋} ∪ {𝑌})) |
| 9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = ({𝑋} ∪ {𝑌})) |
| 10 | | df-pr 4629 |
. . . . . 6
⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌}) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
| 12 | | df-pr 4629 |
. . . . . . . 8
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = ({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) |
| 13 | 12 | dmeqi 5915 |
. . . . . . 7
⊢ dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = dom ({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) |
| 14 | 13 | eqeq1i 2742 |
. . . . . 6
⊢ (dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌} ↔ dom ({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
| 15 | | dmun 5921 |
. . . . . . 7
⊢ dom
({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) = (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) |
| 16 | 15 | eqeq1i 2742 |
. . . . . 6
⊢ (dom
({〈𝑋, 𝐴〉} ∪ {〈𝑌, 𝐵〉}) = {𝑋, 𝑌} ↔ (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
| 17 | 14, 16 | bitri 275 |
. . . . 5
⊢ (dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌} ↔ (dom {〈𝑋, 𝐴〉} ∪ dom {〈𝑌, 𝐵〉}) = {𝑋, 𝑌}) |
| 18 | 11, 17 | sylibr 234 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌}) |
| 19 | | dmsnopg 6233 |
. . . . . 6
⊢ (𝐶 ∈ 𝐻 → dom {〈𝑍, 𝐶〉} = {𝑍}) |
| 20 | 19 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
| 21 | 20 | 3ad2ant2 1135 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑍, 𝐶〉} = {𝑍}) |
| 22 | 18, 21 | uneq12d 4169 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∪ {𝑍})) |
| 23 | | df-tp 4631 |
. . . . 5
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) |
| 24 | 23 | dmeqi 5915 |
. . . 4
⊢ dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = dom ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) |
| 25 | | dmun 5921 |
. . . 4
⊢ dom
({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) = (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ dom {〈𝑍, 𝐶〉}) |
| 26 | 24, 25 | eqtri 2765 |
. . 3
⊢ dom
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ dom {〈𝑍, 𝐶〉}) |
| 27 | | df-tp 4631 |
. . 3
⊢ {𝑋, 𝑌, 𝑍} = ({𝑋, 𝑌} ∪ {𝑍}) |
| 28 | 22, 26, 27 | 3eqtr4g 2802 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = {𝑋, 𝑌, 𝑍}) |
| 29 | | df-fn 6564 |
. 2
⊢
({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍} ↔ (Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} ∧ dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = {𝑋, 𝑌, 𝑍})) |
| 30 | 1, 28, 29 | sylanbrc 583 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍}) |