Metamath Proof Explorer


Theorem sbthlem8

Description: Lemma for sbth . (Contributed by NM, 27-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 𝐴 ∈ V
sbthlem.2 𝐷 = { 𝑥 ∣ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) }
sbthlem.3 𝐻 = ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) )
Assertion sbthlem8 ( ( Fun 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔𝐴 ) ∧ Fun 𝑔 ) ) → Fun 𝐻 )

Proof

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 eqtr3id ( ( ( 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 𝐻 )