domss2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > domss2		Structured version Visualization version GIF version

Theorem domss2 9134

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

**Hypothesis**
Ref	Expression
domss2.1	⊢ 𝐺 = ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))

**Assertion**
Ref	Expression
domss2	⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)))

**Proof of Theorem domss2**
Step	Hyp	Ref	Expression
1		f1f1orn 6839	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
2	1	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→ran 𝐹)
3		simp2 1155	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉)
4		rnexg 7908	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
5	3, 4	syl 18	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐴 ∈ V)
6		uniexg 7751	. . . . . . . . 9 ⊢ (ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V)
7		pwexg 5354	. . . . . . . . 9 ⊢ (∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V)
8	5, 6, 7	3syl 19	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 ∪ ran 𝐴 ∈ V)
9		1stconst 8104	. . . . . . . 8 ⊢ (𝒫 ∪ ran 𝐴 ∈ V → (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹))
10	8, 9	syl 18	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹))
11		difexg 5305	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12	11	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13		disjen 9132	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
14	3, 12, 13	syl2anc 596	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
15	14	simpld 500	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅)
16		disjdif 4436	. . . . . . . 8 ⊢ (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
17	16	a1i 11	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18		f1oun 6847	. . . . . . 7 ⊢ (((𝐹:𝐴–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 𝐹)))
19	2, 10, 15, 17, 18	syl22anc 852	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20		undif2 4441	. . . . . . . 8 ⊢ (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹 ∪ 𝐵)
21		f1f 6781	. . . . . . . . . . 11 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
22	21	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴⟶𝐵)
23	22	frnd 6721	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐹 ⊆ 𝐵)
24		ssequn1 4142	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ 𝐵 ↔ (ran 𝐹 ∪ 𝐵) = 𝐵)
25	23, 24	sylib 221	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ 𝐵) = 𝐵)
26	20, 25	eqtrid 2813	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
27	26	f1oeq3d 6824	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵))
28	19, 27	mpbid 235	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵)
29		f1ocnv 6840	. . . . 5 ⊢ ((𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵 → ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
30	28, 29	syl 18	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
31		domss2.1	. . . . 5 ⊢ 𝐺 = ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
32		f1oeq1 6815	. . . . 5 ⊢ (𝐺 = ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) → (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↔ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
33	31, 32	ax-mp 5	. . . 4 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↔ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
34	30, 33	sylibr 237	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
35		f1ofo 6835	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → 𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
36		forn 6802	. . . . 5 ⊢ (𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
37	34, 35, 36	3syl 19	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
38	37	f1oeq3d 6824	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ↔ 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
39	34, 38	mpbird 260	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→ran 𝐺)
40		ssun1 4134	. . 3 ⊢ 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
41	40, 37	sseqtrrid 3983	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ⊆ ran 𝐺)
42		ssid 3962	. . . 4 ⊢ ran 𝐹 ⊆ ran 𝐹
43		cores 6255	. . . 4 ⊢ (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹))
44	42, 43	ax-mp 5	. . 3 ⊢ ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹)
45		dmres 6016	. . . . . . . . 9 ⊢ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
46		f1ocnv 6840	. . . . . . . . . . . 12 ⊢ ((1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
47		f1odm 6831	. . . . . . . . . . . 12 ⊢ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) → dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = (𝐵 ∖ ran 𝐹))
48	10, 46, 47	3syl 19	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = (𝐵 ∖ ran 𝐹))
49	48	ineq2d 4176	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
50	49, 16	eqtrdi 2817	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = ∅)
51	45, 50	eqtrid 2813	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
52		relres 6009	. . . . . . . . 9 ⊢ Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)
53		reldm0 5923	. . . . . . . . 9 ⊢ (Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) → ((^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅))
54	52, 53	ax-mp 5	. . . . . . . 8 ⊢ ((^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
55	51, 54	sylibr 237	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
56	55	uneq2d 4125	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ ∅))
57		cnvun 6144	. . . . . . . . 9 ⊢ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
58	31, 57	eqtri 2789	. . . . . . . 8 ⊢ 𝐺 = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
59	58	reseq1i 5979	. . . . . . 7 ⊢ (𝐺 ↾ ran 𝐹) = ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹)
60		resundir 5998	. . . . . . 7 ⊢ ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹) = ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
61		df-rn 5677	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
62	61	reseq2i 5980	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ ran 𝐹) = (^◡𝐹 ↾ dom ^◡𝐹)
63		relcnv 6111	. . . . . . . . . 10 ⊢ Rel ^◡𝐹
64		resdm 6030	. . . . . . . . . 10 ⊢ (Rel ^◡𝐹 → (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹
66	62, 65	eqtri 2789	. . . . . . . 8 ⊢ (^◡𝐹 ↾ ran 𝐹) = ^◡𝐹
67	66	uneq1i 4121	. . . . . . 7 ⊢ ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
68	59, 60, 67	3eqtrri 2794	. . . . . 6 ⊢ (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69		un0 4354	. . . . . 6 ⊢ (^◡𝐹 ∪ ∅) = ^◡𝐹
70	56, 68, 69	3eqtr3g 2824	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ↾ ran 𝐹) = ^◡𝐹)
71	70	coeq1d 5852	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (^◡𝐹 ∘ 𝐹))
72		f1cocnv1 6858	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
73	72	3ad2ant1 1151	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
74	71, 73	eqtrd 2801	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
75	44, 74	eqtr3id 2815	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
76	39, 41, 75	3jca 1146	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 Vcvv 3458 ∖ cdif 3905 ∪ cun 3906 ∩ cin 3907 ⊆ wss 3908 ∅c0 4289 𝒫 cpw 4567 {csn 4594 ∪ cuni 4877 class class class wbr 5114 I cid 5560 × cxp 5664 ^◡ccnv 5665 dom cdm 5666 ran crn 5667 ↾ cres 5668 ∘ ccom 5670 Rel wrel 5671 ⟶wf 6539 –1-1→wf1 6540 –onto→wfo 6541 –1-1-onto→wf1o 6542 1^st c1st 7993 ≈ cen 8949

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-1st 7995 df-2nd 7996 df-en 8953

This theorem is used by: domssex2 9135 domssex 9136

W3C validator