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 9112

Description: A corollary of disjenex 9111. 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 6822	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
2	1	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→ran 𝐹)
3		simp2 1153	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉)
4		rnexg 7887	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
5	3, 4	syl 18	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐴 ∈ V)
6		uniexg 7727	. . . . . . . . 9 ⊢ (ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V)
7		pwexg 5339	. . . . . . . . 9 ⊢ (∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V)
8	5, 6, 7	3syl 19	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 ∪ ran 𝐴 ∈ V)
9		1stconst 8083	. . . . . . . 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 5289	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12	11	3ad2ant3 1151	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13		disjen 9110	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
14	3, 12, 13	syl2anc 595	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
15	14	simpld 499	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅)
16		disjdif 4429	. . . . . . . 8 ⊢ (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
17	16	a1i 11	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18		f1oun 6830	. . . . . . 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 851	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20		undif2 4434	. . . . . . . 8 ⊢ (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹 ∪ 𝐵)
21		f1f 6764	. . . . . . . . . . 11 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
22	21	3ad2ant1 1149	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴⟶𝐵)
23	22	frnd 6704	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐹 ⊆ 𝐵)
24		ssequn1 4141	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ 𝐵 ↔ (ran 𝐹 ∪ 𝐵) = 𝐵)
25	23, 24	sylib 221	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ 𝐵) = 𝐵)
26	20, 25	eqtrid 2812	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
27	26	f1oeq3d 6807	. . . . . 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 6823	. . . . 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 6798	. . . . 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 6818	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → 𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
36		forn 6785	. . . . 5 ⊢ (𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
37	34, 35, 36	3syl 19	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
38	37	f1oeq3d 6807	. . 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 4133	. . 3 ⊢ 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
41	40, 37	sseqtrrid 3982	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ⊆ ran 𝐺)
42		ssid 3961	. . . 4 ⊢ ran 𝐹 ⊆ ran 𝐹
43		cores 6239	. . . 4 ⊢ (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹))
44	42, 43	ax-mp 5	. . 3 ⊢ ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹)
45		dmres 6001	. . . . . . . . 9 ⊢ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
46		f1ocnv 6823	. . . . . . . . . . . 12 ⊢ ((1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
47		f1odm 6814	. . . . . . . . . . . 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 4175	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
50	49, 16	eqtrdi 2816	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = ∅)
51	45, 50	eqtrid 2812	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
52		relres 5994	. . . . . . . . 9 ⊢ Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)
53		reldm0 5908	. . . . . . . . 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 4124	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ ∅))
57		cnvun 6129	. . . . . . . . 9 ⊢ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
58	31, 57	eqtri 2788	. . . . . . . 8 ⊢ 𝐺 = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
59	58	reseq1i 5964	. . . . . . 7 ⊢ (𝐺 ↾ ran 𝐹) = ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹)
60		resundir 5983	. . . . . . 7 ⊢ ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹) = ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
61		df-rn 5662	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
62	61	reseq2i 5965	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ ran 𝐹) = (^◡𝐹 ↾ dom ^◡𝐹)
63		relcnv 6096	. . . . . . . . . 10 ⊢ Rel ^◡𝐹
64		resdm 6015	. . . . . . . . . 10 ⊢ (Rel ^◡𝐹 → (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹
66	62, 65	eqtri 2788	. . . . . . . 8 ⊢ (^◡𝐹 ↾ ran 𝐹) = ^◡𝐹
67	66	uneq1i 4120	. . . . . . 7 ⊢ ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
68	59, 60, 67	3eqtrri 2793	. . . . . 6 ⊢ (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69		un0 4351	. . . . . 6 ⊢ (^◡𝐹 ∪ ∅) = ^◡𝐹
70	56, 68, 69	3eqtr3g 2823	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ↾ ran 𝐹) = ^◡𝐹)
71	70	coeq1d 5837	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (^◡𝐹 ∘ 𝐹))
72		f1cocnv1 6841	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
73	72	3ad2ant1 1149	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
74	71, 73	eqtrd 2800	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
75	44, 74	eqtr3id 2814	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
76	39, 41, 75	3jca 1144	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 Vcvv 3457 ∖ cdif 3904 ∪ cun 3905 ∩ cin 3906 ⊆ wss 3907 ∅c0 4288 𝒫 cpw 4558 {csn 4585 ∪ cuni 4867 class class class wbr 5104 I cid 5545 × cxp 5649 ^◡ccnv 5650 dom cdm 5651 ran crn 5652 ↾ cres 5653 ∘ ccom 5655 Rel wrel 5656 ⟶wf 6521 –1-1→wf1 6522 –onto→wfo 6523 –1-1-onto→wf1o 6524 1^st c1st 7972 ≈ cen 8928

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-1st 7974 df-2nd 7975 df-en 8932

This theorem is referenced by: domssex2 9113 domssex 9114

W3C validator