Proof of Theorem metakunt17
Step | Hyp | Ref
| Expression |
1 | | metakunt17.1 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋) |
2 | | metakunt17.2 |
. . . . . 6
⊢ (𝜑 → 𝐻:𝐵–1-1-onto→𝑌) |
3 | | metakunt17.4 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
4 | | metakunt17.7 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∩ 𝑌) = ∅) |
5 | 3, 4 | jca 516 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∩ 𝐵) = ∅ ∧ (𝑋 ∩ 𝑌) = ∅)) |
6 | 1, 2, 5 | jca31 519 |
. . . . 5
⊢ (𝜑 → ((𝐺:𝐴–1-1-onto→𝑋 ∧ 𝐻:𝐵–1-1-onto→𝑌) ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (𝑋 ∩ 𝑌) = ∅))) |
7 | | f1oun 6614 |
. . . . 5
⊢ (((𝐺:𝐴–1-1-onto→𝑋 ∧ 𝐻:𝐵–1-1-onto→𝑌) ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (𝑋 ∩ 𝑌) = ∅)) → (𝐺 ∪ 𝐻):(𝐴 ∪ 𝐵)–1-1-onto→(𝑋 ∪ 𝑌)) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 ∪ 𝐻):(𝐴 ∪ 𝐵)–1-1-onto→(𝑋 ∪ 𝑌)) |
9 | | metakunt17.3 |
. . . 4
⊢ (𝜑 → 𝐼:𝐶–1-1-onto→𝑍) |
10 | | indir 4176 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
11 | | metakunt17.5 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) |
12 | | metakunt17.6 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅) |
13 | 11, 12 | uneq12d 4065 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = (∅ ∪
∅)) |
14 | | 0un 4282 |
. . . . . . . 8
⊢ (∅
∪ ∅) = ∅ |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∅ ∪ ∅) =
∅) |
16 | 13, 15 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ∅) |
17 | 10, 16 | syl5eq 2806 |
. . . . 5
⊢ (𝜑 → ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅) |
18 | | indir 4176 |
. . . . . 6
⊢ ((𝑋 ∪ 𝑌) ∩ 𝑍) = ((𝑋 ∩ 𝑍) ∪ (𝑌 ∩ 𝑍)) |
19 | | metakunt17.8 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∩ 𝑍) = ∅) |
20 | | metakunt17.9 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∩ 𝑍) = ∅) |
21 | 19, 20 | uneq12d 4065 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ∩ 𝑍) ∪ (𝑌 ∩ 𝑍)) = (∅ ∪
∅)) |
22 | 21, 15 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ∩ 𝑍) ∪ (𝑌 ∩ 𝑍)) = ∅) |
23 | 18, 22 | syl5eq 2806 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∪ 𝑌) ∩ 𝑍) = ∅) |
24 | 17, 23 | jca 516 |
. . . 4
⊢ (𝜑 → (((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅ ∧ ((𝑋 ∪ 𝑌) ∩ 𝑍) = ∅)) |
25 | 8, 9, 24 | jca31 519 |
. . 3
⊢ (𝜑 → (((𝐺 ∪ 𝐻):(𝐴 ∪ 𝐵)–1-1-onto→(𝑋 ∪ 𝑌) ∧ 𝐼:𝐶–1-1-onto→𝑍) ∧ (((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅ ∧ ((𝑋 ∪ 𝑌) ∩ 𝑍) = ∅))) |
26 | | f1oun 6614 |
. . 3
⊢ ((((𝐺 ∪ 𝐻):(𝐴 ∪ 𝐵)–1-1-onto→(𝑋 ∪ 𝑌) ∧ 𝐼:𝐶–1-1-onto→𝑍) ∧ (((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅ ∧ ((𝑋 ∪ 𝑌) ∩ 𝑍) = ∅)) → ((𝐺 ∪ 𝐻) ∪ 𝐼):((𝐴 ∪ 𝐵) ∪ 𝐶)–1-1-onto→((𝑋 ∪ 𝑌) ∪ 𝑍)) |
27 | 25, 26 | syl 17 |
. 2
⊢ (𝜑 → ((𝐺 ∪ 𝐻) ∪ 𝐼):((𝐴 ∪ 𝐵) ∪ 𝐶)–1-1-onto→((𝑋 ∪ 𝑌) ∪ 𝑍)) |
28 | | metakunt17.10 |
. . 3
⊢ (𝜑 → 𝐹 = ((𝐺 ∪ 𝐻) ∪ 𝐼)) |
29 | | metakunt17.11 |
. . 3
⊢ (𝜑 → 𝐷 = ((𝐴 ∪ 𝐵) ∪ 𝐶)) |
30 | | metakunt17.12 |
. . 3
⊢ (𝜑 → 𝑊 = ((𝑋 ∪ 𝑌) ∪ 𝑍)) |
31 | 28, 29, 30 | f1oeq123d 6589 |
. 2
⊢ (𝜑 → (𝐹:𝐷–1-1-onto→𝑊 ↔ ((𝐺 ∪ 𝐻) ∪ 𝐼):((𝐴 ∪ 𝐵) ∪ 𝐶)–1-1-onto→((𝑋 ∪ 𝑌) ∪ 𝑍))) |
32 | 27, 31 | mpbird 260 |
1
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝑊) |