sbthlem8

	Ref	Expression
Hypotheses	sbthlem.1	$⊢ A \in V$
	sbthlem.2	$⊢ D = \{x \| (x \subseteq A \land g [B ∖ f [x]] \subseteq A ∖ x)\}$
	sbthlem.3	$⊢ H = ({f ↾}_{⋃ D}) \cup ({g^{-1} ↾}_{(A ∖ ⋃ D)})$
Assertion	sbthlem8	$⊢ (Fun f^{-1} \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to Fun H^{-1}$

Proof

Step	Hyp	Ref	Expression
1		sbthlem.1	$⊢ A \in V$
2		sbthlem.2	$⊢ D = \{x \| (x \subseteq A \land g [B ∖ f [x]] \subseteq A ∖ x)\}$
3		sbthlem.3	$⊢ H = ({f ↾}_{⋃ D}) \cup ({g^{-1} ↾}_{(A ∖ ⋃ D)})$
4		funres11	$⊢ Fun f^{-1} \to Fun {({f ↾}_{⋃ D})}^{-1}$
5		funcnvcnv	$⊢ Fun g \to Fun {g^{-1}}^{-1}$
6		funres11	$⊢ Fun {g^{-1}}^{-1} \to Fun {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1}$
7	5 6	syl	$⊢ Fun g \to Fun {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1}$
8	7	ad3antrrr	$⊢ (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1}) \to Fun {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1}$
9	4 8	anim12i	$⊢ (Fun f^{-1} \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to (Fun {({f ↾}_{⋃ D})}^{-1} \land 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 \land ran g \subseteq A) \land Fun g^{-1}) \to g^{-1} [A ∖ ⋃ D] = B ∖ f [⋃ D]$
17	15 16	eqtr3id	$⊢ ((dom g = B \land ran g \subseteq A) \land Fun g^{-1}) \to dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = B ∖ f [⋃ D]$
18		ineq12	$⊢ (dom {({f ↾}_{⋃ D})}^{-1} = f [⋃ D] \land dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = B ∖ f [⋃ D]) \to dom {({f ↾}_{⋃ D})}^{-1} \cap dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = f [⋃ D] \cap (B ∖ f [⋃ D])$
19	12 17 18	sylancr	$⊢ ((dom g = B \land ran g \subseteq A) \land Fun g^{-1}) \to dom {({f ↾}_{⋃ D})}^{-1} \cap dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = f [⋃ D] \cap (B ∖ f [⋃ D])$
20		disjdif	$⊢ f [⋃ D] \cap (B ∖ f [⋃ D]) = \emptyset$
21	19 20	eqtrdi	$⊢ ((dom g = B \land ran g \subseteq A) \land Fun g^{-1}) \to dom {({f ↾}_{⋃ D})}^{-1} \cap dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = \emptyset$
22	21	adantlll	$⊢ (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1}) \to dom {({f ↾}_{⋃ D})}^{-1} \cap dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = \emptyset$
23	22	adantl	$⊢ (Fun f^{-1} \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to dom {({f ↾}_{⋃ D})}^{-1} \cap dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = \emptyset$
24		funun	$⊢ ((Fun {({f ↾}_{⋃ D})}^{-1} \land Fun {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1}) \land dom {({f ↾}_{⋃ D})}^{-1} \cap dom {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1} = \emptyset) \to Fun ({({f ↾}_{⋃ D})}^{-1} \cup {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1})$
25	9 23 24	syl2anc	$⊢ (Fun f^{-1} \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to Fun ({({f ↾}_{⋃ D})}^{-1} \cup {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1})$
26	3	cnveqi	$⊢ H^{-1} = {(({f ↾}_{⋃ D}) \cup ({g^{-1} ↾}_{(A ∖ ⋃ D)}))}^{-1}$
27		cnvun	$⊢ {(({f ↾}_{⋃ D}) \cup ({g^{-1} ↾}_{(A ∖ ⋃ D)}))}^{-1} = {({f ↾}_{⋃ D})}^{-1} \cup {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1}$
28	26 27	eqtri	$⊢ H^{-1} = {({f ↾}_{⋃ D})}^{-1} \cup {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1}$
29	28	funeqi	$⊢ Fun H^{-1} \leftrightarrow Fun ({({f ↾}_{⋃ D})}^{-1} \cup {({g^{-1} ↾}_{(A ∖ ⋃ D)})}^{-1})$
30	25 29	sylibr	$⊢ (Fun f^{-1} \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to Fun H^{-1}$

Metamath Proof Explorer

Theorem sbthlem8

Proof