Metamath Proof Explorer

Theorem sbthlem8

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

Ref Expression
Hypotheses sbthlem.1 $⊢ A ∈ V$
sbthlem.2 $⊢ D = x | x ⊆ A ∧ g B ∖ f x ⊆ A ∖ x$
sbthlem.3 $⊢ H = f ↾ ⋃ D ∪ g -1 ↾ A ∖ ⋃ D$
Assertion sbthlem8 $⊢ Fun ⁡ f -1 ∧ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → Fun ⁡ H -1$

Proof

Step Hyp Ref Expression
1 sbthlem.1 $⊢ A ∈ V$
2 sbthlem.2 $⊢ D = x | x ⊆ A ∧ g B ∖ f x ⊆ A ∖ x$
3 sbthlem.3 $⊢ H = f ↾ ⋃ D ∪ g -1 ↾ A ∖ ⋃ D$
4 funres11 $⊢ Fun ⁡ f -1 → Fun ⁡ f ↾ ⋃ D -1$
5 funcnvcnv $⊢ Fun ⁡ g → Fun ⁡ g -1 -1$
6 funres11 $⊢ Fun ⁡ g -1 -1 → Fun ⁡ g -1 ↾ A ∖ ⋃ D -1$
7 5 6 syl $⊢ Fun ⁡ g → Fun ⁡ g -1 ↾ A ∖ ⋃ D -1$
8 7 ad3antrrr $⊢ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → Fun ⁡ g -1 ↾ A ∖ ⋃ D -1$
9 4 8 anim12i $⊢ Fun ⁡ f -1 ∧ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → Fun ⁡ f ↾ ⋃ D -1 ∧ Fun ⁡ g -1 ↾ A ∖ ⋃ D -1$
10 df-ima $⊢ f ⋃ D = ran ⁡ f ↾ ⋃ D$
11 df-rn $⊢ ran ⁡ f ↾ ⋃ D = dom ⁡ f ↾ ⋃ D -1$
12 10 11 eqtr2i $⊢ dom ⁡ f ↾ ⋃ D -1 = f ⋃ D$
13 df-ima $⊢ g -1 A ∖ ⋃ D = ran ⁡ g -1 ↾ A ∖ ⋃ D$
14 df-rn $⊢ ran ⁡ g -1 ↾ A ∖ ⋃ D = dom ⁡ g -1 ↾ A ∖ ⋃ D -1$
15 13 14 eqtri $⊢ g -1 A ∖ ⋃ D = dom ⁡ g -1 ↾ A ∖ ⋃ D -1$
16 1 2 sbthlem4 $⊢ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → g -1 A ∖ ⋃ D = B ∖ f ⋃ D$
17 15 16 syl5eqr $⊢ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = B ∖ f ⋃ D$
18 ineq12 $⊢ dom ⁡ f ↾ ⋃ D -1 = f ⋃ D ∧ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = B ∖ f ⋃ D → dom ⁡ f ↾ ⋃ D -1 ∩ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = f ⋃ D ∩ B ∖ f ⋃ D$
19 12 17 18 sylancr $⊢ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → dom ⁡ f ↾ ⋃ D -1 ∩ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = f ⋃ D ∩ B ∖ f ⋃ D$
20 disjdif $⊢ f ⋃ D ∩ B ∖ f ⋃ D = ∅$
21 19 20 eqtrdi $⊢ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → dom ⁡ f ↾ ⋃ D -1 ∩ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = ∅$
22 21 adantlll $⊢ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → dom ⁡ f ↾ ⋃ D -1 ∩ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = ∅$
23 22 adantl $⊢ Fun ⁡ f -1 ∧ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → dom ⁡ f ↾ ⋃ D -1 ∩ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = ∅$
24 funun $⊢ Fun ⁡ f ↾ ⋃ D -1 ∧ Fun ⁡ g -1 ↾ A ∖ ⋃ D -1 ∧ dom ⁡ f ↾ ⋃ D -1 ∩ dom ⁡ g -1 ↾ A ∖ ⋃ D -1 = ∅ → Fun ⁡ f ↾ ⋃ D -1 ∪ g -1 ↾ A ∖ ⋃ D -1$
25 9 23 24 syl2anc $⊢ Fun ⁡ f -1 ∧ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → Fun ⁡ f ↾ ⋃ D -1 ∪ g -1 ↾ A ∖ ⋃ D -1$
26 3 cnveqi $⊢ H -1 = f ↾ ⋃ D ∪ g -1 ↾ A ∖ ⋃ D -1$
27 cnvun $⊢ f ↾ ⋃ D ∪ g -1 ↾ A ∖ ⋃ D -1 = f ↾ ⋃ D -1 ∪ g -1 ↾ A ∖ ⋃ D -1$
28 26 27 eqtri $⊢ H -1 = f ↾ ⋃ D -1 ∪ g -1 ↾ A ∖ ⋃ D -1$
29 28 funeqi $⊢ Fun ⁡ H -1 ↔ Fun ⁡ f ↾ ⋃ D -1 ∪ g -1 ↾ A ∖ ⋃ D -1$
30 25 29 sylibr $⊢ Fun ⁡ f -1 ∧ Fun ⁡ g ∧ dom ⁡ g = B ∧ ran ⁡ g ⊆ A ∧ Fun ⁡ g -1 → Fun ⁡ H -1$