# Metamath Proof Explorer

## Theorem sbthlem7

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

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

### Proof

Step Hyp Ref Expression
1 sbthlem.1 𝐴 ∈ V
2 sbthlem.2 𝐷 = { 𝑥 ∣ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) }
3 sbthlem.3 𝐻 = ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) )
4 funres ( Fun 𝑓 → Fun ( 𝑓 𝐷 ) )
5 funres ( Fun 𝑔 → Fun ( 𝑔 ↾ ( 𝐴 𝐷 ) ) )
6 dmres dom ( 𝑓 𝐷 ) = ( 𝐷 ∩ dom 𝑓 )
7 inss1 ( 𝐷 ∩ dom 𝑓 ) ⊆ 𝐷
8 6 7 eqsstri dom ( 𝑓 𝐷 ) ⊆ 𝐷
9 ssrin ( dom ( 𝑓 𝐷 ) ⊆ 𝐷 → ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ( 𝐷 ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) )
10 8 9 ax-mp ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ( 𝐷 ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) )
11 dmres dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) = ( ( 𝐴 𝐷 ) ∩ dom 𝑔 )
12 inss1 ( ( 𝐴 𝐷 ) ∩ dom 𝑔 ) ⊆ ( 𝐴 𝐷 )
13 11 12 eqsstri dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ⊆ ( 𝐴 𝐷 )
14 sslin ( dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ⊆ ( 𝐴 𝐷 ) → ( 𝐷 ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ( 𝐷 ∩ ( 𝐴 𝐷 ) ) )
15 13 14 ax-mp ( 𝐷 ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ( 𝐷 ∩ ( 𝐴 𝐷 ) )
16 10 15 sstri ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ( 𝐷 ∩ ( 𝐴 𝐷 ) )
17 disjdif ( 𝐷 ∩ ( 𝐴 𝐷 ) ) = ∅
18 16 17 sseqtri ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ∅
19 ss0 ( ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ⊆ ∅ → ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) = ∅ )
20 18 19 ax-mp ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) = ∅
21 funun ( ( ( Fun ( 𝑓 𝐷 ) ∧ Fun ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ∧ ( dom ( 𝑓 𝐷 ) ∩ dom ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) = ∅ ) → Fun ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) )
22 20 21 mpan2 ( ( Fun ( 𝑓 𝐷 ) ∧ Fun ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) → Fun ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) )
23 4 5 22 syl2an ( ( Fun 𝑓 ∧ Fun 𝑔 ) → Fun ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) )
24 3 funeqi ( Fun 𝐻 ↔ Fun ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) )
25 23 24 sylibr ( ( Fun 𝑓 ∧ Fun 𝑔 ) → Fun 𝐻 )