Proof of Theorem sbthlemi9
Step | Hyp | Ref
| Expression |
1 | | simp2 983 |
. . . . . . . . . 10
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝑓:𝐴–1-1→𝐵) |
2 | | df-f1 5178 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝐵 ↔ (𝑓:𝐴⟶𝐵 ∧ Fun ◡𝑓)) |
3 | 1, 2 | sylib 121 |
. . . . . . . . 9
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (𝑓:𝐴⟶𝐵 ∧ Fun ◡𝑓)) |
4 | 3 | simpld 111 |
. . . . . . . 8
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝑓:𝐴⟶𝐵) |
5 | | df-f 5177 |
. . . . . . . 8
⊢ (𝑓:𝐴⟶𝐵 ↔ (𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵)) |
6 | 4, 5 | sylib 121 |
. . . . . . 7
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵)) |
7 | 6 | simpld 111 |
. . . . . 6
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝑓 Fn 𝐴) |
8 | | df-fn 5176 |
. . . . . 6
⊢ (𝑓 Fn 𝐴 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝐴)) |
9 | 7, 8 | sylib 121 |
. . . . 5
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (Fun 𝑓 ∧ dom 𝑓 = 𝐴)) |
10 | 9 | simpld 111 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun 𝑓) |
11 | | simp3 984 |
. . . . . 6
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝑔:𝐵–1-1→𝐴) |
12 | | df-f1 5178 |
. . . . . 6
⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔)) |
13 | 11, 12 | sylib 121 |
. . . . 5
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔)) |
14 | 13 | simprd 113 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun ◡𝑔) |
15 | | sbthlem.1 |
. . . . 5
⊢ 𝐴 ∈ V |
16 | | sbthlem.2 |
. . . . 5
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
17 | | sbthlem.3 |
. . . . 5
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
18 | 15, 16, 17 | sbthlem7 6910 |
. . . 4
⊢ ((Fun
𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) |
19 | 10, 14, 18 | syl2anc 409 |
. . 3
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun 𝐻) |
20 | | simp1 982 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) →
EXMID) |
21 | 9 | simprd 113 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom 𝑓 = 𝐴) |
22 | 13 | simpld 111 |
. . . . . 6
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝑔:𝐵⟶𝐴) |
23 | | df-f 5177 |
. . . . . 6
⊢ (𝑔:𝐵⟶𝐴 ↔ (𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
24 | 22, 23 | sylib 121 |
. . . . 5
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
25 | 24 | simprd 113 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran 𝑔 ⊆ 𝐴) |
26 | 15, 16, 17 | sbthlemi5 6908 |
. . . 4
⊢
((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴)) → dom 𝐻 = 𝐴) |
27 | 20, 21, 25, 26 | syl12anc 1218 |
. . 3
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom 𝐻 = 𝐴) |
28 | | df-fn 5176 |
. . 3
⊢ (𝐻 Fn 𝐴 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐴)) |
29 | 19, 27, 28 | sylanbrc 414 |
. 2
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻 Fn 𝐴) |
30 | 3 | simprd 113 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun ◡𝑓) |
31 | 24 | simpld 111 |
. . . . . 6
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝑔 Fn 𝐵) |
32 | | df-fn 5176 |
. . . . . 6
⊢ (𝑔 Fn 𝐵 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝐵)) |
33 | 31, 32 | sylib 121 |
. . . . 5
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (Fun 𝑔 ∧ dom 𝑔 = 𝐵)) |
34 | 33, 25 | jca 304 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴)) |
35 | 15, 16, 17 | sbthlemi8 6911 |
. . . 4
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |
36 | 20, 30, 34, 14, 35 | syl22anc 1221 |
. . 3
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun ◡𝐻) |
37 | 6 | simprd 113 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran 𝑓 ⊆ 𝐵) |
38 | 33 | simprd 113 |
. . . . 5
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom 𝑔 = 𝐵) |
39 | 38, 25 | jca 304 |
. . . 4
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴)) |
40 | | df-rn 4600 |
. . . . 5
⊢ ran 𝐻 = dom ◡𝐻 |
41 | 15, 16, 17 | sbthlemi6 6909 |
. . . . 5
⊢
(((EXMID ∧ ran 𝑓 ⊆ 𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) |
42 | 40, 41 | eqtr3id 2204 |
. . . 4
⊢
(((EXMID ∧ ran 𝑓 ⊆ 𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → dom ◡𝐻 = 𝐵) |
43 | 20, 37, 39, 14, 42 | syl22anc 1221 |
. . 3
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom ◡𝐻 = 𝐵) |
44 | | df-fn 5176 |
. . 3
⊢ (◡𝐻 Fn 𝐵 ↔ (Fun ◡𝐻 ∧ dom ◡𝐻 = 𝐵)) |
45 | 36, 43, 44 | sylanbrc 414 |
. 2
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ◡𝐻 Fn 𝐵) |
46 | | dff1o4 5425 |
. 2
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻 Fn 𝐴 ∧ ◡𝐻 Fn 𝐵)) |
47 | 29, 45, 46 | sylanbrc 414 |
1
⊢
((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |