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	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∃ 𝑔 ( 𝑔 : 𝐵 –1-1→ V ∧ ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fex2	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐹 ∈ V )
3	1 2	syl3an1	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐹 ∈ V )
4		f1stres	⊢ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ⟶ ( 𝐵 ∖ ran 𝐹 )
5		difexg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∖ ran 𝐹 ) ∈ V )
6	5	3ad2ant3	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∖ ran 𝐹 ) ∈ V )
7		snex	⊢ { 𝒫 ∪ ran 𝐴 } ∈ V
8		xpexg	⊢ ( ( ( 𝐵 ∖ ran 𝐹 ) ∈ V ∧ { 𝒫 ∪ ran 𝐴 } ∈ V ) → ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V )
9	6 7 8	sylancl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V )
10		fex2	⊢ ( ( ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ⟶ ( 𝐵 ∖ ran 𝐹 ) ∧ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V ∧ ( 𝐵 ∖ ran 𝐹 ) ∈ V ) → ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V )
11	4 9 6 10	mp3an2i	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V )
12		unexg	⊢ ( ( 𝐹 ∈ V ∧ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V ) → ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
13	3 11 12	syl2anc	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
14		cnvexg	⊢ ( ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
15	13 14	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
16		eqid	⊢ ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) = ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) )
17	16	domss2	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ 𝐴 ⊆ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )
18	17	simp1d	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
19		f1of1	⊢ ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
20	18 19	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
21		ssv	⊢ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ⊆ V
22		f1ss	⊢ ( ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ ran ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ⊆ V ) → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V )
23	20 21 22	sylancl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V )
24	17	simp3d	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
25	23 24	jca	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V ∧ ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )
26		f1eq1	⊢ ( 𝑔 = ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝑔 : 𝐵 –1-1→ V ↔ ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V ) )
27		coeq1	⊢ ( 𝑔 = ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝑔 ∘ 𝐹 ) = ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) )
28	27	eqeq1d	⊢ ( 𝑔 = ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ↔ ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )
29	26 28	anbi12d	⊢ ( 𝑔 = ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( ( 𝑔 : 𝐵 –1-1→ V ∧ ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ↔ ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V ∧ ( ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) )
30	15 25 29	spcedv	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∃ 𝑔 ( 𝑔 : 𝐵 –1-1→ V ∧ ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )

Metamath Proof Explorer

Theorem domssex2

Proof