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