Step |
Hyp |
Ref |
Expression |
1 |
|
sbthlem.1 |
⊢ 𝐴 ∈ V |
2 |
|
sbthlem.2 |
⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) } |
3 |
|
sbthlem.3 |
⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
4 |
|
funres11 |
⊢ ( Fun ◡ 𝑓 → Fun ◡ ( 𝑓 ↾ ∪ 𝐷 ) ) |
5 |
|
funcnvcnv |
⊢ ( Fun 𝑔 → Fun ◡ ◡ 𝑔 ) |
6 |
|
funres11 |
⊢ ( Fun ◡ ◡ 𝑔 → Fun ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
7 |
5 6
|
syl |
⊢ ( Fun 𝑔 → Fun ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
8 |
7
|
ad3antrrr |
⊢ ( ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → Fun ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
9 |
4 8
|
anim12i |
⊢ ( ( Fun ◡ 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∧ Fun ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ) |
10 |
|
df-ima |
⊢ ( 𝑓 “ ∪ 𝐷 ) = ran ( 𝑓 ↾ ∪ 𝐷 ) |
11 |
|
df-rn |
⊢ ran ( 𝑓 ↾ ∪ 𝐷 ) = dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) |
12 |
10 11
|
eqtr2i |
⊢ dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) = ( 𝑓 “ ∪ 𝐷 ) |
13 |
|
df-ima |
⊢ ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) |
14 |
|
df-rn |
⊢ ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) = dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) |
15 |
13 14
|
eqtri |
⊢ ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) |
16 |
1 2
|
sbthlem4 |
⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) |
17 |
15 16
|
syl5eqr |
⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) |
18 |
|
ineq12 |
⊢ ( ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) = ( 𝑓 “ ∪ 𝐷 ) ∧ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) → ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∩ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ( 𝑓 “ ∪ 𝐷 ) ∩ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) |
19 |
12 17 18
|
sylancr |
⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∩ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ( 𝑓 “ ∪ 𝐷 ) ∩ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) |
20 |
|
disjdif |
⊢ ( ( 𝑓 “ ∪ 𝐷 ) ∩ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ∅ |
21 |
19 20
|
eqtrdi |
⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∩ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ∅ ) |
22 |
21
|
adantlll |
⊢ ( ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∩ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ∅ ) |
23 |
22
|
adantl |
⊢ ( ( Fun ◡ 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∩ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ∅ ) |
24 |
|
funun |
⊢ ( ( ( Fun ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∧ Fun ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ∧ ( dom ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∩ dom ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ∅ ) → Fun ( ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∪ ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ) |
25 |
9 23 24
|
syl2anc |
⊢ ( ( Fun ◡ 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → Fun ( ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∪ ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ) |
26 |
3
|
cnveqi |
⊢ ◡ 𝐻 = ◡ ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
27 |
|
cnvun |
⊢ ◡ ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∪ ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
28 |
26 27
|
eqtri |
⊢ ◡ 𝐻 = ( ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∪ ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) |
29 |
28
|
funeqi |
⊢ ( Fun ◡ 𝐻 ↔ Fun ( ◡ ( 𝑓 ↾ ∪ 𝐷 ) ∪ ◡ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ) |
30 |
25 29
|
sylibr |
⊢ ( ( Fun ◡ 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → Fun ◡ 𝐻 ) |