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 8647 |
. . . . . . 7
⊢ ((Fun
𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) |
5 | 1, 2, 3 | sbthlem5 8645 |
. . . . . . . 8
⊢ ((dom
𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴) |
6 | 5 | adantrl 716 |
. . . . . . 7
⊢ ((dom
𝑓 = 𝐴 ∧ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) → dom 𝐻 = 𝐴) |
7 | 4, 6 | anim12i 616 |
. . . . . 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 8648 |
. . . 4
⊢ ((Fun
◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |
12 | 11 | adantll 714 |
. . 3
⊢ (((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |
13 | | simpr 489 |
. . . . . . 7
⊢ ((Fun
𝑔 ∧ dom 𝑔 = 𝐵) → dom 𝑔 = 𝐵) |
14 | 13 | anim1i 618 |
. . . . . 6
⊢ (((Fun
𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) → (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
15 | | df-rn 5528 |
. . . . . . 7
⊢ ran 𝐻 = dom ◡𝐻 |
16 | 1, 2, 3 | sbthlem6 8646 |
. . . . . . 7
⊢ ((ran
𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) |
17 | 15, 16 | syl5eqr 2808 |
. . . . . 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 520 |
. 2
⊢ (((((Fun
𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵))) |
22 | | df-f1 6333 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 ↔ (𝑓:𝐴⟶𝐵 ∧ Fun ◡𝑓)) |
23 | | df-f 6332 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 ↔ (𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵)) |
24 | | df-fn 6331 |
. . . . . . 7
⊢ (𝑓 Fn 𝐴 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝐴)) |
25 | 24 | anbi1i 627 |
. . . . . 6
⊢ ((𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ↔ ((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵)) |
26 | 23, 25 | bitri 278 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 ↔ ((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵)) |
27 | 26 | anbi1i 627 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ Fun ◡𝑓) ↔ (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓)) |
28 | 22, 27 | bitri 278 |
. . 3
⊢ (𝑓:𝐴–1-1→𝐵 ↔ (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓)) |
29 | | df-f1 6333 |
. . . 4
⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔)) |
30 | | df-f 6332 |
. . . . . 6
⊢ (𝑔:𝐵⟶𝐴 ↔ (𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
31 | | df-fn 6331 |
. . . . . . 7
⊢ (𝑔 Fn 𝐵 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝐵)) |
32 | 31 | anbi1i 627 |
. . . . . 6
⊢ ((𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ↔ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) |
33 | 30, 32 | bitri 278 |
. . . . 5
⊢ (𝑔:𝐵⟶𝐴 ↔ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) |
34 | 33 | anbi1i 627 |
. . . 4
⊢ ((𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔) ↔ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) |
35 | 29, 34 | bitri 278 |
. . 3
⊢ (𝑔:𝐵–1-1→𝐴 ↔ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) |
36 | 28, 35 | anbi12i 630 |
. 2
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ ((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓 ⊆ 𝐵) ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔))) |
37 | | dff1o4 6603 |
. . 3
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻 Fn 𝐴 ∧ ◡𝐻 Fn 𝐵)) |
38 | | df-fn 6331 |
. . . 4
⊢ (𝐻 Fn 𝐴 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
39 | | df-fn 6331 |
. . . 4
⊢ (◡𝐻 Fn 𝐵 ↔ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵)) |
40 | 38, 39 | anbi12i 630 |
. . 3
⊢ ((𝐻 Fn 𝐴 ∧ ◡𝐻 Fn 𝐵) ↔ ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵))) |
41 | 37, 40 | bitri 278 |
. 2
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵))) |
42 | 21, 36, 41 | 3imtr4i 296 |
1
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |