Proof of Theorem sbthlem9
| Step | Hyp | Ref
| Expression |
| 1 | | sbthlem.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
| 2 | | sbthlem.2 |
. . . . . . . 8
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
| 3 | | sbthlem.3 |
. . . . . . . 8
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
| 4 | 1, 2, 3 | sbthlem7 9129 |
. . . . . . 7
⊢ ((Fun
𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) |
| 5 | 1, 2, 3 | sbthlem5 9127 |
. . . . . . . 8
⊢ ((dom
𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴) |
| 6 | 5 | adantrl 716 |
. . . . . . 7
⊢ ((dom
𝑓 = 𝐴 ∧ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) → dom 𝐻 = 𝐴) |
| 7 | 4, 6 | anim12i 613 |
. . . . . 6
⊢ (((Fun
𝑓 ∧ Fun ◡𝑔) ∧ (dom 𝑓 = 𝐴 ∧ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴))) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
| 8 | 7 | an42s 661 |
. . . . 5
⊢ (((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
| 9 | 8 | adantlr 715 |
. . . 4
⊢ ((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
| 10 | 9 | adantlr 715 |
. . 3
⊢ (((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
| 11 | 1, 2, 3 | sbthlem8 9130 |
. . . 4
⊢ ((Fun
◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |
| 12 | 11 | adantll 714 |
. . 3
⊢ (((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |
| 13 | | simpr 484 |
. . . . . . 7
⊢ ((Fun
𝑔 ∧ dom 𝑔 = 𝐵) → dom 𝑔 = 𝐵) |
| 14 | 13 | anim1i 615 |
. . . . . 6
⊢ (((Fun
𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) → (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
| 15 | | df-rn 5696 |
. . . . . . 7
⊢ ran 𝐻 = dom ◡𝐻 |
| 16 | 1, 2, 3 | sbthlem6 9128 |
. . . . . . 7
⊢ ((ran
𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) |
| 17 | 15, 16 | eqtr3id 2791 |
. . . . . 6
⊢ ((ran
𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → dom ◡𝐻 = 𝐵) |
| 18 | 14, 17 | sylanr1 682 |
. . . . 5
⊢ ((ran
𝑓 ⊆ 𝐵 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → dom ◡𝐻 = 𝐵) |
| 19 | 18 | adantll 714 |
. . . 4
⊢ ((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → dom ◡𝐻 = 𝐵) |
| 20 | 19 | adantlr 715 |
. . 3
⊢ (((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → dom ◡𝐻 = 𝐵) |
| 21 | 10, 12, 20 | jca32 515 |
. 2
⊢ (((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵))) |
| 22 | | df-f1 6566 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 ↔ (𝑓:𝐴⟶𝐵 ∧ Fun ◡𝑓)) |
| 23 | | df-f 6565 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 ↔ (𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵)) |
| 24 | | df-fn 6564 |
. . . . . . 7
⊢ (𝑓 Fn 𝐴 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝐴)) |
| 25 | 24 | anbi1i 624 |
. . . . . 6
⊢ ((𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ↔ ((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵)) |
| 26 | 23, 25 | bitri 275 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 ↔ ((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵)) |
| 27 | 26 | anbi1i 624 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ Fun ◡𝑓) ↔ (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓)) |
| 28 | 22, 27 | bitri 275 |
. . 3
⊢ (𝑓:𝐴–1-1→𝐵 ↔ (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓)) |
| 29 | | df-f1 6566 |
. . . 4
⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔)) |
| 30 | | df-f 6565 |
. . . . . 6
⊢ (𝑔:𝐵⟶𝐴 ↔ (𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
| 31 | | df-fn 6564 |
. . . . . . 7
⊢ (𝑔 Fn 𝐵 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝐵)) |
| 32 | 31 | anbi1i 624 |
. . . . . 6
⊢ ((𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ↔ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) |
| 33 | 30, 32 | bitri 275 |
. . . . 5
⊢ (𝑔:𝐵⟶𝐴 ↔ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) |
| 34 | 33 | anbi1i 624 |
. . . 4
⊢ ((𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔) ↔ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) |
| 35 | 29, 34 | bitri 275 |
. . 3
⊢ (𝑔:𝐵–1-1→𝐴 ↔ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) |
| 36 | 28, 35 | anbi12i 628 |
. 2
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ ((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔))) |
| 37 | | dff1o4 6856 |
. . 3
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻 Fn 𝐴 ∧ ◡𝐻 Fn 𝐵)) |
| 38 | | df-fn 6564 |
. . . 4
⊢ (𝐻 Fn 𝐴 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
| 39 | | df-fn 6564 |
. . . 4
⊢ (◡𝐻 Fn 𝐵 ↔ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵)) |
| 40 | 38, 39 | anbi12i 628 |
. . 3
⊢ ((𝐻 Fn 𝐴 ∧ ◡𝐻 Fn 𝐵) ↔ ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵))) |
| 41 | 37, 40 | bitri 275 |
. 2
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵))) |
| 42 | 21, 36, 41 | 3imtr4i 292 |
1
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |