domss2

Description: A corollary of disjenex . If F is an injection from A to B then G is a right inverse of F from B to a superset of A . (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Hypothesis	domss2.1	$⊢ G = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
	Assertion	domss2	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (G : B \underset{1-1 onto}{⟶} ran G \land A \subseteq ran G \land G \circ F = {I ↾}_{A})$

Proof

Step	Hyp	Ref	Expression
1		domss2.1	$⊢ G = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
2		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
3	2	3ad2ant1	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to F : A \underset{1-1 onto}{⟶} ran F$
4		simp2	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to A \in V$
5		rnexg	$⊢ A \in V \to ran A \in V$
6	4 5	syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran A \in V$
7		uniexg	$⊢ ran A \in V \to ⋃ ran A \in V$
8		pwexg	$⊢ ⋃ ran A \in V \to 𝒫 ⋃ ran A \in V$
9	6 7 8	3syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to 𝒫 ⋃ ran A \in V$
10		1stconst	$⊢ 𝒫 ⋃ ran A \in V \to ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \underset{1-1 onto}{⟶} B ∖ ran F$
11	9 10	syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \underset{1-1 onto}{⟶} B ∖ ran F$
12		difexg	$⊢ B \in W \to B ∖ ran F \in V$
13	12	3ad2ant3	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to B ∖ ran F \in V$
14		disjen	$⊢ (A \in V \land B ∖ ran F \in V) \to (A \cap ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) = \emptyset \land ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \approx (B ∖ ran F))$
15	4 13 14	syl2anc	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (A \cap ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) = \emptyset \land ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \approx (B ∖ ran F))$
16	15	simpld	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to A \cap ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) = \emptyset$
17		disjdif	$⊢ ran F \cap (B ∖ ran F) = \emptyset$
18	17	a1i	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran F \cap (B ∖ ran F) = \emptyset$
19		f1oun	$⊢ ((F : A \underset{1-1 onto}{⟶} ran F \land ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \underset{1-1 onto}{⟶} B ∖ ran F) \land (A \cap ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) = \emptyset \land ran F \cap (B ∖ ran F) = \emptyset)) \to (F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})) : A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \underset{1-1 onto}{⟶} ran F \cup (B ∖ ran F)$
20	3 11 16 18 19	syl22anc	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})) : A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \underset{1-1 onto}{⟶} ran F \cup (B ∖ ran F)$
21		undif2	$⊢ ran F \cup (B ∖ ran F) = ran F \cup B$
22		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
23	22	3ad2ant1	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to F : A ⟶ B$
24	23	frnd	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran F \subseteq B$
25		ssequn1	$⊢ ran F \subseteq B \leftrightarrow ran F \cup B = B$
26	24 25	sylib	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran F \cup B = B$
27	21 26	syl5eq	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran F \cup (B ∖ ran F) = B$
28	27	f1oeq3d	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ((F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})) : A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \underset{1-1 onto}{⟶} ran F \cup (B ∖ ran F) \leftrightarrow (F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})) : A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \underset{1-1 onto}{⟶} B)$
29	20 28	mpbid	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})) : A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \underset{1-1 onto}{⟶} B$
30		f1ocnv	$⊢ (F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})) : A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \underset{1-1 onto}{⟶} B \to {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
31	29 30	syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
32		f1oeq1	$⊢ G = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to (G : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \leftrightarrow {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}))$
33	1 32	ax-mp	$⊢ G : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \leftrightarrow {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
34	31 33	sylibr	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to G : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
35		f1ofo	$⊢ G : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \to G : B \underset{onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
36		forn	$⊢ G : B \underset{onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}) \to ran G = A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
37	34 35 36	3syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran G = A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
38	37	f1oeq3d	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (G : B \underset{1-1 onto}{⟶} ran G \leftrightarrow G : B \underset{1-1 onto}{⟶} A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\}))$
39	34 38	mpbird	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to G : B \underset{1-1 onto}{⟶} ran G$
40		ssun1	$⊢ A \subseteq A \cup ((B ∖ ran F) \times \{𝒫 ⋃ ran A\})$
41	40 37	sseqtrrid	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to A \subseteq ran G$
42		ssid	$⊢ ran F \subseteq ran F$
43		cores	$⊢ ran F \subseteq ran F \to ({G ↾}_{ran F}) \circ F = G \circ F$
44	42 43	ax-mp	$⊢ ({G ↾}_{ran F}) \circ F = G \circ F$
45		dmres	$⊢ dom ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = ran F \cap dom {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1}$
46		f1ocnv	$⊢ ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \underset{1-1 onto}{⟶} B ∖ ran F \to {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} : B ∖ ran F \underset{1-1 onto}{⟶} (B ∖ ran F) \times \{𝒫 ⋃ ran A\}$
47		f1odm	$⊢ {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} : B ∖ ran F \underset{1-1 onto}{⟶} (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \to dom {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} = B ∖ ran F$
48	11 46 47	3syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to dom {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} = B ∖ ran F$
49	48	ineq2d	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran F \cap dom {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} = ran F \cap (B ∖ ran F)$
50	49 17	eqtrdi	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ran F \cap dom {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} = \emptyset$
51	45 50	syl5eq	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to dom ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = \emptyset$
52		relres	$⊢ Rel ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F})$
53		reldm0	$⊢ Rel ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) \to ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F} = \emptyset \leftrightarrow dom ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = \emptyset)$
54	52 53	ax-mp	$⊢ {{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F} = \emptyset \leftrightarrow dom ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = \emptyset$
55	51 54	sylibr	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to {{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F} = \emptyset$
56	55	uneq2d	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to F^{-1} \cup ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = F^{-1} \cup \emptyset$
57		cnvun	$⊢ {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} = F^{-1} \cup {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1}$
58	1 57	eqtri	$⊢ G = F^{-1} \cup {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1}$
59	58	reseq1i	$⊢ {G ↾}_{ran F} = {(F^{-1} \cup {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1}) ↾}_{ran F}$
60		resundir	$⊢ {(F^{-1} \cup {({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1}) ↾}_{ran F} = ({F^{-1} ↾}_{ran F}) \cup ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F})$
61		df-rn	$⊢ ran F = dom F^{-1}$
62	61	reseq2i	$⊢ {F^{-1} ↾}_{ran F} = {F^{-1} ↾}_{dom F^{-1}}$
63		relcnv	$⊢ Rel F^{-1}$
64		resdm	$⊢ Rel F^{-1} \to {F^{-1} ↾}_{dom F^{-1}} = F^{-1}$
65	63 64	ax-mp	$⊢ {F^{-1} ↾}_{dom F^{-1}} = F^{-1}$
66	62 65	eqtri	$⊢ {F^{-1} ↾}_{ran F} = F^{-1}$
67	66	uneq1i	$⊢ ({F^{-1} ↾}_{ran F}) \cup ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = F^{-1} \cup ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F})$
68	59 60 67	3eqtrri	$⊢ F^{-1} \cup ({{({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})})}^{-1} ↾}_{ran F}) = {G ↾}_{ran F}$
69		un0	$⊢ F^{-1} \cup \emptyset = F^{-1}$
70	56 68 69	3eqtr3g	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to {G ↾}_{ran F} = F^{-1}$
71	70	coeq1d	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ({G ↾}_{ran F}) \circ F = F^{-1} \circ F$
72		f1cocnv1	$⊢ F : A \underset{1-1}{⟶} B \to F^{-1} \circ F = {I ↾}_{A}$
73	72	3ad2ant1	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to F^{-1} \circ F = {I ↾}_{A}$
74	71 73	eqtrd	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to ({G ↾}_{ran F}) \circ F = {I ↾}_{A}$
75	44 74	syl5eqr	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to G \circ F = {I ↾}_{A}$
76	39 41 75	3jca	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (G : B \underset{1-1 onto}{⟶} ran G \land A \subseteq ran G \land G \circ F = {I ↾}_{A})$

Metamath Proof Explorer

Theorem domss2

Proof