Proof of Theorem ftpg
| Step | Hyp | Ref
| Expression |
| 1 | | 3simpa 1149 |
. . . 4
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉)) |
| 2 | | 3simpa 1149 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺)) |
| 3 | | simp1 1137 |
. . . 4
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → 𝑋 ≠ 𝑌) |
| 4 | | fprg 7175 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺) ∧ 𝑋 ≠ 𝑌) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}:{𝑋, 𝑌}⟶{𝐴, 𝐵}) |
| 5 | 1, 2, 3, 4 | syl3an 1161 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}:{𝑋, 𝑌}⟶{𝐴, 𝐵}) |
| 6 | | eqidd 2738 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑍, 𝐶〉} = {〈𝑍, 𝐶〉}) |
| 7 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑍 ∈ 𝑊) |
| 8 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → 𝐶 ∈ 𝐻) |
| 9 | 7, 8 | anim12i 613 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻)) → (𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻)) |
| 10 | 9 | 3adant3 1133 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻)) |
| 11 | | fsng 7157 |
. . . . 5
⊢ ((𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻) → ({〈𝑍, 𝐶〉}:{𝑍}⟶{𝐶} ↔ {〈𝑍, 𝐶〉} = {〈𝑍, 𝐶〉})) |
| 12 | 10, 11 | syl 17 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ({〈𝑍, 𝐶〉}:{𝑍}⟶{𝐶} ↔ {〈𝑍, 𝐶〉} = {〈𝑍, 𝐶〉})) |
| 13 | 6, 12 | mpbird 257 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑍, 𝐶〉}:{𝑍}⟶{𝐶}) |
| 14 | | elpri 4649 |
. . . . . . . 8
⊢ (𝑍 ∈ {𝑋, 𝑌} → (𝑍 = 𝑋 ∨ 𝑍 = 𝑌)) |
| 15 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑋 ↔ 𝑋 = 𝑍) |
| 16 | | nne 2944 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ≠ 𝑍 ↔ 𝑋 = 𝑍) |
| 17 | 15, 16 | bitr4i 278 |
. . . . . . . . . 10
⊢ (𝑍 = 𝑋 ↔ ¬ 𝑋 ≠ 𝑍) |
| 18 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑌 ↔ 𝑌 = 𝑍) |
| 19 | | nne 2944 |
. . . . . . . . . . 11
⊢ (¬
𝑌 ≠ 𝑍 ↔ 𝑌 = 𝑍) |
| 20 | 18, 19 | bitr4i 278 |
. . . . . . . . . 10
⊢ (𝑍 = 𝑌 ↔ ¬ 𝑌 ≠ 𝑍) |
| 21 | 17, 20 | orbi12i 915 |
. . . . . . . . 9
⊢ ((𝑍 = 𝑋 ∨ 𝑍 = 𝑌) ↔ (¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
| 22 | | ianor 984 |
. . . . . . . . 9
⊢ (¬
(𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) ↔ (¬ 𝑋 ≠ 𝑍 ∨ ¬ 𝑌 ≠ 𝑍)) |
| 23 | 21, 22 | sylbb2 238 |
. . . . . . . 8
⊢ ((𝑍 = 𝑋 ∨ 𝑍 = 𝑌) → ¬ (𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
| 24 | 14, 23 | syl 17 |
. . . . . . 7
⊢ (𝑍 ∈ {𝑋, 𝑌} → ¬ (𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) |
| 25 | 24 | con2i 139 |
. . . . . 6
⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ¬ 𝑍 ∈ {𝑋, 𝑌}) |
| 26 | 25 | 3adant1 1131 |
. . . . 5
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ¬ 𝑍 ∈ {𝑋, 𝑌}) |
| 27 | 26 | 3ad2ant3 1136 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ¬ 𝑍 ∈ {𝑋, 𝑌}) |
| 28 | | disjsn 4711 |
. . . 4
⊢ (({𝑋, 𝑌} ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ {𝑋, 𝑌}) |
| 29 | 27, 28 | sylibr 234 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) |
| 30 | | fun 6770 |
. . 3
⊢
((({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}:{𝑋, 𝑌}⟶{𝐴, 𝐵} ∧ {〈𝑍, 𝐶〉}:{𝑍}⟶{𝐶}) ∧ ({𝑋, 𝑌} ∩ {𝑍}) = ∅) → ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}):({𝑋, 𝑌} ∪ {𝑍})⟶({𝐴, 𝐵} ∪ {𝐶})) |
| 31 | 5, 13, 29, 30 | syl21anc 838 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}):({𝑋, 𝑌} ∪ {𝑍})⟶({𝐴, 𝐵} ∪ {𝐶})) |
| 32 | | df-tp 4631 |
. . . 4
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) |
| 33 | 32 | feq1i 6727 |
. . 3
⊢
({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶} ↔ ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}):{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) |
| 34 | | df-tp 4631 |
. . . 4
⊢ {𝑋, 𝑌, 𝑍} = ({𝑋, 𝑌} ∪ {𝑍}) |
| 35 | | df-tp 4631 |
. . . 4
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
| 36 | 34, 35 | feq23i 6730 |
. . 3
⊢
(({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}):{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶} ↔ ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}):({𝑋, 𝑌} ∪ {𝑍})⟶({𝐴, 𝐵} ∪ {𝐶})) |
| 37 | 33, 36 | bitri 275 |
. 2
⊢
({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶} ↔ ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}):({𝑋, 𝑌} ∪ {𝑍})⟶({𝐴, 𝐵} ∪ {𝐶})) |
| 38 | 31, 37 | sylibr 234 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) |