Step |
Hyp |
Ref |
Expression |
1 |
|
sbthlem.1 |
⊢ 𝐴 ∈ V |
2 |
|
sbthlem.2 |
⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) } |
3 |
|
sbthlem.3 |
⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
4 |
1 2 3
|
sbthlem7 |
⊢ ( ( Fun 𝑓 ∧ Fun ◡ 𝑔 ) → Fun 𝐻 ) |
5 |
1 2 3
|
sbthlem5 |
⊢ ( ( dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴 ) → dom 𝐻 = 𝐴 ) |
6 |
5
|
adantrl |
⊢ ( ( dom 𝑓 = 𝐴 ∧ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ) → dom 𝐻 = 𝐴 ) |
7 |
4 6
|
anim12i |
⊢ ( ( ( Fun 𝑓 ∧ Fun ◡ 𝑔 ) ∧ ( dom 𝑓 = 𝐴 ∧ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ) |
8 |
7
|
an42s |
⊢ ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ) |
9 |
8
|
adantlr |
⊢ ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ) |
10 |
9
|
adantlr |
⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ) |
11 |
1 2 3
|
sbthlem8 |
⊢ ( ( Fun ◡ 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → Fun ◡ 𝐻 ) |
12 |
11
|
adantll |
⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → Fun ◡ 𝐻 ) |
13 |
|
simpr |
⊢ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) → dom 𝑔 = 𝐵 ) |
14 |
13
|
anim1i |
⊢ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) → ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ) |
15 |
|
df-rn |
⊢ ran 𝐻 = dom ◡ 𝐻 |
16 |
1 2 3
|
sbthlem6 |
⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ran 𝐻 = 𝐵 ) |
17 |
15 16
|
syl5eqr |
⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 ) |
18 |
14 17
|
sylanr1 |
⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 ) |
19 |
18
|
adantll |
⊢ ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 ) |
20 |
19
|
adantlr |
⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 ) |
21 |
10 12 20
|
jca32 |
⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ∧ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) ) |
22 |
|
df-f1 |
⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) ) |
23 |
|
df-f |
⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) ) |
24 |
|
df-fn |
⊢ ( 𝑓 Fn 𝐴 ↔ ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ) |
25 |
24
|
anbi1i |
⊢ ( ( 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) ↔ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ) |
26 |
23 25
|
bitri |
⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ) |
27 |
26
|
anbi1i |
⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) ↔ ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ) |
28 |
22 27
|
bitri |
⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ) |
29 |
|
df-f1 |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 ↔ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ Fun ◡ 𝑔 ) ) |
30 |
|
df-f |
⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ ( 𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ) |
31 |
|
df-fn |
⊢ ( 𝑔 Fn 𝐵 ↔ ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ) |
32 |
31
|
anbi1i |
⊢ ( ( 𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ) |
33 |
30 32
|
bitri |
⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ) |
34 |
33
|
anbi1i |
⊢ ( ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ Fun ◡ 𝑔 ) ↔ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) |
35 |
29 34
|
bitri |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 ↔ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) |
36 |
28 35
|
anbi12i |
⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ↔ ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) ) |
37 |
|
dff1o4 |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐻 Fn 𝐴 ∧ ◡ 𝐻 Fn 𝐵 ) ) |
38 |
|
df-fn |
⊢ ( 𝐻 Fn 𝐴 ↔ ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ) |
39 |
|
df-fn |
⊢ ( ◡ 𝐻 Fn 𝐵 ↔ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) |
40 |
38 39
|
anbi12i |
⊢ ( ( 𝐻 Fn 𝐴 ∧ ◡ 𝐻 Fn 𝐵 ) ↔ ( ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ∧ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) ) |
41 |
37 40
|
bitri |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ∧ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) ) |
42 |
21 36 41
|
3imtr4i |
⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 ) |