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