Proof of Theorem oacomf1o
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) |
2 | 1 | oacomf1olem 7531 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∧ (ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∩ 𝐵) = ∅)) |
3 | 2 | simpld 474 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥))) |
4 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) |
5 | 4 | oacomf1olem 7531 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → ((𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):𝐵–1-1-onto→ran
(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) ∧ (ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) ∩ 𝐴) = ∅)) |
6 | 5 | ancoms 468 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):𝐵–1-1-onto→ran
(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) ∧ (ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) ∩ 𝐴) = ∅)) |
7 | 6 | simpld 474 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):𝐵–1-1-onto→ran
(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) |
8 | | f1ocnv 6062 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):𝐵–1-1-onto→ran
(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) → ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))–1-1-onto→𝐵) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))–1-1-onto→𝐵) |
10 | | incom 3767 |
. . . . . 6
⊢ (𝐴 ∩ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) = (ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) ∩ 𝐴) |
11 | 6 | simprd 478 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) ∩ 𝐴) = ∅) |
12 | 10, 11 | syl5eq 2656 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) = ∅) |
13 | 2 | simprd 478 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∩ 𝐵) = ∅) |
14 | | f1oun 6069 |
. . . . 5
⊢ ((((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∧ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)):ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))–1-1-onto→𝐵) ∧ ((𝐴 ∩ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) = ∅ ∧ (ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∩ 𝐵) = ∅)) → ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))):(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵)) |
15 | 3, 9, 12, 13, 14 | syl22anc 1319 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))):(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵)) |
16 | | oacomf1o.1 |
. . . . 5
⊢ 𝐹 = ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) |
17 | | f1oeq1 6040 |
. . . . 5
⊢ (𝐹 = ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) → (𝐹:(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵) ↔ ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))):(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵))) |
18 | 16, 17 | ax-mp 5 |
. . . 4
⊢ (𝐹:(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵) ↔ ((𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))):(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵)) |
19 | 15, 18 | sylibr 223 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵)) |
20 | | oarec 7529 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))) |
21 | | f1oeq2 6041 |
. . . 4
⊢ ((𝐴 +𝑜 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) → (𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵) ↔ 𝐹:(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵))) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵) ↔ 𝐹:(𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵))) |
23 | 19, 22 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵)) |
24 | | oarec 7529 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (𝐵 +𝑜 𝐴) = (𝐵 ∪ ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)))) |
25 | 24 | ancoms 468 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝐴) = (𝐵 ∪ ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)))) |
26 | | uncom 3719 |
. . . 4
⊢ (𝐵 ∪ ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥))) = (ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵) |
27 | 25, 26 | syl6eq 2660 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝐴) = (ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵)) |
28 | | f1oeq3 6042 |
. . 3
⊢ ((𝐵 +𝑜 𝐴) = (ran (𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵) → (𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(𝐵 +𝑜 𝐴) ↔ 𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵))) |
29 | 27, 28 | syl 17 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(𝐵 +𝑜 𝐴) ↔ 𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(ran
(𝑥 ∈ 𝐴 ↦ (𝐵 +𝑜 𝑥)) ∪ 𝐵))) |
30 | 23, 29 | mpbird 246 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐴 +𝑜 𝐵)–1-1-onto→(𝐵 +𝑜 𝐴)) |