domssex2

Description: A corollary of disjenex . If F is an injection from A to B then there is a right inverse g 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
	Assertion	domssex2	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to \exists g (g : B \underset{1-1}{⟶} V \land g \circ F = {I ↾}_{A})$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2		fex2	$⊢ (F : A ⟶ B \land A \in V \land B \in W) \to F \in V$
3	1 2	syl3an1	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to F \in V$
4		f1stres	$⊢ ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran F) \times \{𝒫 ⋃ ran A\} ⟶ B ∖ ran F$
5		difexg	$⊢ B \in W \to B ∖ ran F \in V$
6	5	3ad2ant3	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to B ∖ ran F \in V$
7		snex	$⊢ \{𝒫 ⋃ ran A\} \in V$
8		xpexg	$⊢ (B ∖ ran F \in V \land \{𝒫 ⋃ ran A\} \in V) \to (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \in V$
9	6 7 8	sylancl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \in V$
10		fex2	$⊢ (({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran F) \times \{𝒫 ⋃ ran A\} ⟶ B ∖ ran F \land (B ∖ ran F) \times \{𝒫 ⋃ ran A\} \in V \land B ∖ ran F \in V) \to {1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})} \in V$
11	4 9 6 10	mp3an2i	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to {1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})} \in V$
12		unexg	$⊢ (F \in V \land {1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})} \in V) \to F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) \in V$
13	3 11 12	syl2anc	$⊢ (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\})}) \in V$
14		cnvexg	$⊢ F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}) \in V \to {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V$
15	13 14	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} \in V$
16		eqid	$⊢ {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
17	16	domss2	$⊢ (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}{⟶} ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land A \subseteq ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ F = {I ↾}_{A})$
18	17	simp1d	$⊢ (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}{⟶} ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
19		f1of1	$⊢ {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1}{⟶} ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
20	18 19	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}{⟶} ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
21		ssv	$⊢ ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \subseteq V$
22		f1ss	$⊢ ({(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1}{⟶} ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land ran {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \subseteq V) \to {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1}{⟶} V$
23	20 21 22	sylancl	$⊢ (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}{⟶} V$
24	17	simp3d	$⊢ (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} \circ F = {I ↾}_{A}$
25	23 24	jca	$⊢ (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}{⟶} V \land {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ F = {I ↾}_{A})$
26		f1eq1	$⊢ g = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to (g : B \underset{1-1}{⟶} V \leftrightarrow {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1}{⟶} V)$
27		coeq1	$⊢ g = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to g \circ F = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ F$
28	27	eqeq1d	$⊢ g = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to (g \circ F = {I ↾}_{A} \leftrightarrow {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ F = {I ↾}_{A})$
29	26 28	anbi12d	$⊢ g = {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to ((g : B \underset{1-1}{⟶} V \land g \circ F = {I ↾}_{A}) \leftrightarrow ({(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1}{⟶} V \land {(F \cup ({1^{st} ↾}_{((B ∖ ran F) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ F = {I ↾}_{A}))$
30	15 25 29	spcedv	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to \exists g (g : B \underset{1-1}{⟶} V \land g \circ F = {I ↾}_{A})$

Metamath Proof Explorer

Theorem domssex2

Proof