Metamath Proof Explorer

Theorem 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 ⊢ ( 1st ↾ ( ( 𝐵 ∖ 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 ⊢ ( ( ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ⟶ ( 𝐵 ∖ ran 𝐹 ) ∧ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V ∧ ( 𝐵 ∖ ran 𝐹 ) ∈ V ) → ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V )
11 4 9 6 10 mp3an2i ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V )
12 unexg ⊢ ( ( 𝐹 ∈ V ∧ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V ) → ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
13 3 11 12 syl2anc ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
14 cnvexg ⊢ ( ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
15 13 14 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
16 eqid ⊢ ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) )
17 16 domss2 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ 𝐴 ⊆ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )
18 17 simp1d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
19 f1of1 ⊢ ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
20 18 19 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
21 ssv ⊢ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ⊆ V
22 f1ss ⊢ ( ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ ran ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ⊆ V ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V )
23 20 21 22 sylancl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V )
24 17 simp3d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
25 23 24 jca ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V ∧ ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )
26 f1eq1 ⊢ ( 𝑔 = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝑔 : 𝐵 –1-1→ V ↔ ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V ) )
27 coeq1 ⊢ ( 𝑔 = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝑔 ∘ 𝐹 ) = ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) )
28 27 eqeq1d ⊢ ( 𝑔 = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ↔ ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )
29 26 28 anbi12d ⊢ ( 𝑔 = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( ( 𝑔 : 𝐵 –1-1→ V ∧ ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ↔ ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1→ V ∧ ( ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) )
30 15 25 29 spcedv ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∃ 𝑔 ( 𝑔 : 𝐵 –1-1→ V ∧ ( 𝑔 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )