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 9106

Description: A corollary of disjenex 9105. 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 6814	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
2	1	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→ran 𝐹)
3		simp2 1137	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉)
4		rnexg 7881	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
5	3, 4	syl 17	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐴 ∈ V)
6		uniexg 7719	. . . . . . . . 9 ⊢ (ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V)
7		pwexg 5336	. . . . . . . . 9 ⊢ (∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V)
8	5, 6, 7	3syl 18	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 ∪ ran 𝐴 ∈ V)
9		1stconst 8082	. . . . . . . 8 ⊢ (𝒫 ∪ ran 𝐴 ∈ V → (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹))
10	8, 9	syl 17	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹))
11		difexg 5287	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12	11	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13		disjen 9104	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
14	3, 12, 13	syl2anc 584	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
15	14	simpld 494	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅)
16		disjdif 4438	. . . . . . . 8 ⊢ (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
17	16	a1i 11	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18		f1oun 6822	. . . . . . 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 838	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20		undif2 4443	. . . . . . . 8 ⊢ (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹 ∪ 𝐵)
21		f1f 6759	. . . . . . . . . . 11 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
22	21	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴⟶𝐵)
23	22	frnd 6699	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐹 ⊆ 𝐵)
24		ssequn1 4152	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ 𝐵 ↔ (ran 𝐹 ∪ 𝐵) = 𝐵)
25	23, 24	sylib 218	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ 𝐵) = 𝐵)
26	20, 25	eqtrid 2777	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
27	26	f1oeq3d 6800	. . . . . 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 232	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵)
29		f1ocnv 6815	. . . . 5 ⊢ ((𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵 → ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
30	28, 29	syl 17	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
31		domss2.1	. . . . 5 ⊢ 𝐺 = ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
32		f1oeq1 6791	. . . . 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 234	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
35		f1ofo 6810	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → 𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
36		forn 6778	. . . . 5 ⊢ (𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
37	34, 35, 36	3syl 18	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
38	37	f1oeq3d 6800	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ↔ 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
39	34, 38	mpbird 257	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→ran 𝐺)
40		ssun1 4144	. . 3 ⊢ 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
41	40, 37	sseqtrrid 3993	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ⊆ ran 𝐺)
42		ssid 3972	. . . 4 ⊢ ran 𝐹 ⊆ ran 𝐹
43		cores 6225	. . . 4 ⊢ (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹))
44	42, 43	ax-mp 5	. . 3 ⊢ ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹)
45		dmres 5986	. . . . . . . . 9 ⊢ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
46		f1ocnv 6815	. . . . . . . . . . . 12 ⊢ ((1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
47		f1odm 6807	. . . . . . . . . . . 12 ⊢ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) → dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = (𝐵 ∖ ran 𝐹))
48	10, 46, 47	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = (𝐵 ∖ ran 𝐹))
49	48	ineq2d 4186	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
50	49, 16	eqtrdi 2781	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = ∅)
51	45, 50	eqtrid 2777	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
52		relres 5979	. . . . . . . . 9 ⊢ Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)
53		reldm0 5894	. . . . . . . . 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 234	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
56	55	uneq2d 4134	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ ∅))
57		cnvun 6118	. . . . . . . . 9 ⊢ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
58	31, 57	eqtri 2753	. . . . . . . 8 ⊢ 𝐺 = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
59	58	reseq1i 5949	. . . . . . 7 ⊢ (𝐺 ↾ ran 𝐹) = ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹)
60		resundir 5968	. . . . . . 7 ⊢ ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹) = ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
61		df-rn 5652	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
62	61	reseq2i 5950	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ ran 𝐹) = (^◡𝐹 ↾ dom ^◡𝐹)
63		relcnv 6078	. . . . . . . . . 10 ⊢ Rel ^◡𝐹
64		resdm 6000	. . . . . . . . . 10 ⊢ (Rel ^◡𝐹 → (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹
66	62, 65	eqtri 2753	. . . . . . . 8 ⊢ (^◡𝐹 ↾ ran 𝐹) = ^◡𝐹
67	66	uneq1i 4130	. . . . . . 7 ⊢ ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
68	59, 60, 67	3eqtrri 2758	. . . . . 6 ⊢ (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69		un0 4360	. . . . . 6 ⊢ (^◡𝐹 ∪ ∅) = ^◡𝐹
70	56, 68, 69	3eqtr3g 2788	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ↾ ran 𝐹) = ^◡𝐹)
71	70	coeq1d 5828	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (^◡𝐹 ∘ 𝐹))
72		f1cocnv1 6833	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
73	72	3ad2ant1 1133	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
74	71, 73	eqtrd 2765	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
75	44, 74	eqtr3id 2779	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
76	39, 41, 75	3jca 1128	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 Vcvv 3450 ∖ cdif 3914 ∪ cun 3915 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 {csn 4592 ∪ cuni 4874 class class class wbr 5110 I cid 5535 × cxp 5639 ^◡ccnv 5640 dom cdm 5641 ran crn 5642 ↾ cres 5643 ∘ ccom 5645 Rel wrel 5646 ⟶wf 6510 –1-1→wf1 6511 –onto→wfo 6512 –1-1-onto→wf1o 6513 1^st c1st 7969 ≈ cen 8918

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-1st 7971 df-2nd 7972 df-en 8922

This theorem is referenced by: domssex2 9107 domssex 9108

W3C validator