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 8923

Description: A corollary of disjenex 8922. 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 6727	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
2	1	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→ran 𝐹)
3		simp2 1136	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉)
4		rnexg 7751	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
5	3, 4	syl 17	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐴 ∈ V)
6		uniexg 7593	. . . . . . . . 9 ⊢ (ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V)
7		pwexg 5301	. . . . . . . . 9 ⊢ (∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V)
8	5, 6, 7	3syl 18	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 ∪ ran 𝐴 ∈ V)
9		1stconst 7940	. . . . . . . 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 5251	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12	11	3ad2ant3 1134	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13		disjen 8921	. . . . . . . . 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 495	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅)
16		disjdif 4405	. . . . . . . 8 ⊢ (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
17	16	a1i 11	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18		f1oun 6735	. . . . . . 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 836	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20		undif2 4410	. . . . . . . 8 ⊢ (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹 ∪ 𝐵)
21		f1f 6670	. . . . . . . . . . 11 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
22	21	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴⟶𝐵)
23	22	frnd 6608	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐹 ⊆ 𝐵)
24		ssequn1 4114	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ 𝐵 ↔ (ran 𝐹 ∪ 𝐵) = 𝐵)
25	23, 24	sylib 217	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ 𝐵) = 𝐵)
26	20, 25	eqtrid 2790	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
27	26	f1oeq3d 6713	. . . . . 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 231	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵)
29		f1ocnv 6728	. . . . 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 6704	. . . . 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 233	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
35		f1ofo 6723	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → 𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
36		forn 6691	. . . . 5 ⊢ (𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
37	34, 35, 36	3syl 18	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
38	37	f1oeq3d 6713	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ↔ 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
39	34, 38	mpbird 256	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→ran 𝐺)
40		ssun1 4106	. . 3 ⊢ 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
41	40, 37	sseqtrrid 3974	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ⊆ ran 𝐺)
42		ssid 3943	. . . 4 ⊢ ran 𝐹 ⊆ ran 𝐹
43		cores 6153	. . . 4 ⊢ (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹))
44	42, 43	ax-mp 5	. . 3 ⊢ ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹)
45		dmres 5913	. . . . . . . . 9 ⊢ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
46		f1ocnv 6728	. . . . . . . . . . . 12 ⊢ ((1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
47		f1odm 6720	. . . . . . . . . . . 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 4146	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
50	49, 16	eqtrdi 2794	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = ∅)
51	45, 50	eqtrid 2790	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
52		relres 5920	. . . . . . . . 9 ⊢ Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)
53		reldm0 5837	. . . . . . . . 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 233	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
56	55	uneq2d 4097	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ ∅))
57		cnvun 6046	. . . . . . . . 9 ⊢ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
58	31, 57	eqtri 2766	. . . . . . . 8 ⊢ 𝐺 = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
59	58	reseq1i 5887	. . . . . . 7 ⊢ (𝐺 ↾ ran 𝐹) = ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹)
60		resundir 5906	. . . . . . 7 ⊢ ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹) = ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
61		df-rn 5600	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
62	61	reseq2i 5888	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ ran 𝐹) = (^◡𝐹 ↾ dom ^◡𝐹)
63		relcnv 6012	. . . . . . . . . 10 ⊢ Rel ^◡𝐹
64		resdm 5936	. . . . . . . . . 10 ⊢ (Rel ^◡𝐹 → (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹
66	62, 65	eqtri 2766	. . . . . . . 8 ⊢ (^◡𝐹 ↾ ran 𝐹) = ^◡𝐹
67	66	uneq1i 4093	. . . . . . 7 ⊢ ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
68	59, 60, 67	3eqtrri 2771	. . . . . 6 ⊢ (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69		un0 4324	. . . . . 6 ⊢ (^◡𝐹 ∪ ∅) = ^◡𝐹
70	56, 68, 69	3eqtr3g 2801	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ↾ ran 𝐹) = ^◡𝐹)
71	70	coeq1d 5770	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (^◡𝐹 ∘ 𝐹))
72		f1cocnv1 6746	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
73	72	3ad2ant1 1132	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
74	71, 73	eqtrd 2778	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
75	44, 74	eqtr3id 2792	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
76	39, 41, 75	3jca 1127	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 Vcvv 3432 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 𝒫 cpw 4533 {csn 4561 ∪ cuni 4839 class class class wbr 5074 I cid 5488 × cxp 5587 ^◡ccnv 5588 dom cdm 5589 ran crn 5590 ↾ cres 5591 ∘ ccom 5593 Rel wrel 5594 ⟶wf 6429 –1-1→wf1 6430 –onto→wfo 6431 –1-1-onto→wf1o 6432 1^st c1st 7829 ≈ cen 8730

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-1st 7831 df-2nd 7832 df-en 8734

This theorem is referenced by: domssex2 8924 domssex 8925

W3C validator