sbthlem9

	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	sbthlem9	$⊢ (f : A \underset{1-1}{⟶} B \land g : B \underset{1-1}{⟶} A) \to H : A \underset{1-1 onto}{⟶} B$

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	1 2 3	sbthlem7	$⊢ (Fun f \land Fun g^{-1}) \to Fun H$
5	1 2 3	sbthlem5	$⊢ (dom f = A \land ran g \subseteq A) \to dom H = A$
6	5	adantrl	$⊢ (dom f = A \land ((Fun g \land dom g = B) \land ran g \subseteq A)) \to dom H = A$
7	4 6	anim12i	$⊢ ((Fun f \land Fun g^{-1}) \land (dom f = A \land ((Fun g \land dom g = B) \land ran g \subseteq A))) \to (Fun H \land dom H = A)$
8	7	an42s	$⊢ ((Fun f \land dom f = A) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to (Fun H \land dom H = A)$
9	8	adantlr	$⊢ (((Fun f \land dom f = A) \land ran f \subseteq B) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to (Fun H \land dom H = A)$
10	9	adantlr	$⊢ ((((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1}) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to (Fun H \land dom H = A)$
11	1 2 3	sbthlem8	$⊢ (Fun f^{-1} \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to Fun H^{-1}$
12	11	adantll	$⊢ ((((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1}) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to Fun H^{-1}$
13		simpr	$⊢ (Fun g \land dom g = B) \to dom g = B$
14	13	anim1i	$⊢ ((Fun g \land dom g = B) \land ran g \subseteq A) \to (dom g = B \land ran g \subseteq A)$
15		df-rn	$⊢ ran H = dom H^{-1}$
16	1 2 3	sbthlem6	$⊢ (ran f \subseteq B \land ((dom g = B \land ran g \subseteq A) \land Fun g^{-1})) \to ran H = B$
17	15 16	syl5eqr	$⊢ (ran f \subseteq B \land ((dom g = B \land ran g \subseteq A) \land Fun g^{-1})) \to dom H^{-1} = B$
18	14 17	sylanr1	$⊢ (ran f \subseteq B \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to dom H^{-1} = B$
19	18	adantll	$⊢ (((Fun f \land dom f = A) \land ran f \subseteq B) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to dom H^{-1} = B$
20	19	adantlr	$⊢ ((((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1}) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to dom H^{-1} = B$
21	10 12 20	jca32	$⊢ ((((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1}) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})) \to ((Fun H \land dom H = A) \land (Fun H^{-1} \land dom H^{-1} = B))$
22		df-f1	$⊢ f : A \underset{1-1}{⟶} B \leftrightarrow (f : A ⟶ B \land Fun f^{-1})$
23		df-f	$⊢ f : A ⟶ B \leftrightarrow (f Fn A \land ran f \subseteq B)$
24		df-fn	$⊢ f Fn A \leftrightarrow (Fun f \land dom f = A)$
25	24	anbi1i	$⊢ (f Fn A \land ran f \subseteq B) \leftrightarrow ((Fun f \land dom f = A) \land ran f \subseteq B)$
26	23 25	bitri	$⊢ f : A ⟶ B \leftrightarrow ((Fun f \land dom f = A) \land ran f \subseteq B)$
27	26	anbi1i	$⊢ (f : A ⟶ B \land Fun f^{-1}) \leftrightarrow (((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1})$
28	22 27	bitri	$⊢ f : A \underset{1-1}{⟶} B \leftrightarrow (((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1})$
29		df-f1	$⊢ g : B \underset{1-1}{⟶} A \leftrightarrow (g : B ⟶ A \land Fun g^{-1})$
30		df-f	$⊢ g : B ⟶ A \leftrightarrow (g Fn B \land ran g \subseteq A)$
31		df-fn	$⊢ g Fn B \leftrightarrow (Fun g \land dom g = B)$
32	31	anbi1i	$⊢ (g Fn B \land ran g \subseteq A) \leftrightarrow ((Fun g \land dom g = B) \land ran g \subseteq A)$
33	30 32	bitri	$⊢ g : B ⟶ A \leftrightarrow ((Fun g \land dom g = B) \land ran g \subseteq A)$
34	33	anbi1i	$⊢ (g : B ⟶ A \land Fun g^{-1}) \leftrightarrow (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})$
35	29 34	bitri	$⊢ g : B \underset{1-1}{⟶} A \leftrightarrow (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1})$
36	28 35	anbi12i	$⊢ (f : A \underset{1-1}{⟶} B \land g : B \underset{1-1}{⟶} A) \leftrightarrow ((((Fun f \land dom f = A) \land ran f \subseteq B) \land Fun f^{-1}) \land (((Fun g \land dom g = B) \land ran g \subseteq A) \land Fun g^{-1}))$
37		dff1o4	$⊢ H : A \underset{1-1 onto}{⟶} B \leftrightarrow (H Fn A \land H^{-1} Fn B)$
38		df-fn	$⊢ H Fn A \leftrightarrow (Fun H \land dom H = A)$
39		df-fn	$⊢ H^{-1} Fn B \leftrightarrow (Fun H^{-1} \land dom H^{-1} = B)$
40	38 39	anbi12i	$⊢ (H Fn A \land H^{-1} Fn B) \leftrightarrow ((Fun H \land dom H = A) \land (Fun H^{-1} \land dom H^{-1} = B))$
41	37 40	bitri	$⊢ H : A \underset{1-1 onto}{⟶} B \leftrightarrow ((Fun H \land dom H = A) \land (Fun H^{-1} \land dom H^{-1} = B))$
42	21 36 41	3imtr4i	$⊢ (f : A \underset{1-1}{⟶} B \land g : B \underset{1-1}{⟶} A) \to H : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem sbthlem9

Proof