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	⊢ 𝐺 = ^◡ ( 𝐹 ∪ ( 1^st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) )
	Assertion	domss2	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐺 : 𝐵 –1-1-onto→ ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) )

Proof

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

Metamath Proof Explorer

Theorem domss2

Proof