Proof of Theorem f1un
| Step | Hyp | Ref
| Expression |
| 1 | | f1f 6804 |
. . . 4
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
| 2 | 1 | frnd 6744 |
. . 3
⊢ (𝐹:𝐴–1-1→𝐵 → ran 𝐹 ⊆ 𝐵) |
| 3 | | f1f 6804 |
. . . 4
⊢ (𝐺:𝐶–1-1→𝐷 → 𝐺:𝐶⟶𝐷) |
| 4 | 3 | frnd 6744 |
. . 3
⊢ (𝐺:𝐶–1-1→𝐷 → ran 𝐺 ⊆ 𝐷) |
| 5 | | unss12 4188 |
. . 3
⊢ ((ran
𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐷) → (ran 𝐹 ∪ ran 𝐺) ⊆ (𝐵 ∪ 𝐷)) |
| 6 | 2, 4, 5 | syl2an 596 |
. 2
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) → (ran 𝐹 ∪ ran 𝐺) ⊆ (𝐵 ∪ 𝐷)) |
| 7 | | f1f1orn 6859 |
. . . . 5
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
| 8 | | f1f1orn 6859 |
. . . . 5
⊢ (𝐺:𝐶–1-1→𝐷 → 𝐺:𝐶–1-1-onto→ran
𝐺) |
| 9 | 7, 8 | anim12i 613 |
. . . 4
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) → (𝐹:𝐴–1-1-onto→ran
𝐹 ∧ 𝐺:𝐶–1-1-onto→ran
𝐺)) |
| 10 | | simprl 771 |
. . . . 5
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐴 ∩ 𝐶) = ∅) |
| 11 | | ss2in 4245 |
. . . . . . . 8
⊢ ((ran
𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐷) → (ran 𝐹 ∩ ran 𝐺) ⊆ (𝐵 ∩ 𝐷)) |
| 12 | 2, 4, 11 | syl2an 596 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) → (ran 𝐹 ∩ ran 𝐺) ⊆ (𝐵 ∩ 𝐷)) |
| 13 | | sseq0 4403 |
. . . . . . 7
⊢ (((ran
𝐹 ∩ ran 𝐺) ⊆ (𝐵 ∩ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (ran 𝐹 ∩ ran 𝐺) = ∅) |
| 14 | 12, 13 | sylan 580 |
. . . . . 6
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (ran 𝐹 ∩ ran 𝐺) = ∅) |
| 15 | 14 | adantrl 716 |
. . . . 5
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (ran 𝐹 ∩ ran 𝐺) = ∅) |
| 16 | 10, 15 | jca 511 |
. . . 4
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → ((𝐴 ∩ 𝐶) = ∅ ∧ (ran 𝐹 ∩ ran 𝐺) = ∅)) |
| 17 | | f1oun 6867 |
. . . 4
⊢ (((𝐹:𝐴–1-1-onto→ran
𝐹 ∧ 𝐺:𝐶–1-1-onto→ran
𝐺) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (ran 𝐹 ∩ ran 𝐺) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(ran
𝐹 ∪ ran 𝐺)) |
| 18 | 9, 16, 17 | syl2an2r 685 |
. . 3
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(ran
𝐹 ∪ ran 𝐺)) |
| 19 | | f1of1 6847 |
. . 3
⊢ ((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(ran
𝐹 ∪ ran 𝐺) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(ran 𝐹 ∪ ran 𝐺)) |
| 20 | 18, 19 | syl 17 |
. 2
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(ran 𝐹 ∪ ran 𝐺)) |
| 21 | | f1ss 6809 |
. . 3
⊢ (((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(ran 𝐹 ∪ ran 𝐺) ∧ (ran 𝐹 ∪ ran 𝐺) ⊆ (𝐵 ∪ 𝐷)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(𝐵 ∪ 𝐷)) |
| 22 | 21 | ancoms 458 |
. 2
⊢ (((ran
𝐹 ∪ ran 𝐺) ⊆ (𝐵 ∪ 𝐷) ∧ (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(ran 𝐹 ∪ ran 𝐺)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(𝐵 ∪ 𝐷)) |
| 23 | 6, 20, 22 | syl2an2r 685 |
1
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(𝐵 ∪ 𝐷)) |