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 8004

Description: A corollary of disjenex 8003. 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 6061	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
2	1	3ad2ant1 1075	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→ran 𝐹)
3		simp2 1055	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉)
4		rnexg 6990	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
5	3, 4	syl 17	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐴 ∈ V)
6		uniexg 6853	. . . . . . . . 9 ⊢ (ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V)
7		pwexg 4776	. . . . . . . . 9 ⊢ (∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V)
8	5, 6, 7	3syl 18	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 ∪ ran 𝐴 ∈ V)
9		1stconst 7152	. . . . . . . 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 4735	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12	11	3ad2ant3 1077	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13		disjen 8002	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
14	3, 12, 13	syl2anc 691	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
15	14	simpld 474	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = ∅)
16		disjdif 3992	. . . . . . . 8 ⊢ (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
17	16	a1i 11	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18		f1oun 6069	. . . . . . 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 1319	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20		undif2 3996	. . . . . . . 8 ⊢ (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹 ∪ 𝐵)
21		f1f 6014	. . . . . . . . . . 11 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
22	21	3ad2ant1 1075	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹:𝐴⟶𝐵)
23		frn 5966	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
24	22, 23	syl 17	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐹 ⊆ 𝐵)
25		ssequn1 3745	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ 𝐵 ↔ (ran 𝐹 ∪ 𝐵) = 𝐵)
26	24, 25	sylib 207	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ 𝐵) = 𝐵)
27	20, 26	syl5eq 2656	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
28		f1oeq3 6042	. . . . . . 7 ⊢ ((ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵 → ((𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵))
29	27, 28	syl 17	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵))
30	19, 29	mpbid 221	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵)
31		f1ocnv 6062	. . . . 5 ⊢ ((𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))–1-1-onto→𝐵 → ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
32	30, 31	syl 17	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
33		domss2.1	. . . . 5 ⊢ 𝐺 = ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
34		f1oeq1 6040	. . . . 5 ⊢ (𝐺 = ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) → (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↔ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
35	33, 34	ax-mp 5	. . . 4 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↔ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))):𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
36	32, 35	sylibr 223	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
37		f1ofo 6057	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → 𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
38		forn 6031	. . . . 5 ⊢ (𝐺:𝐵–onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
39	36, 37, 38	3syl 18	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
40		f1oeq3 6042	. . . 4 ⊢ (ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) → (𝐺:𝐵–1-1-onto→ran 𝐺 ↔ 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
41	39, 40	syl 17	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ↔ 𝐺:𝐵–1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))))
42	36, 41	mpbird 246	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐺:𝐵–1-1-onto→ran 𝐺)
43		ssun1 3738	. . 3 ⊢ 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
44	43, 39	syl5sseqr 3617	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ⊆ ran 𝐺)
45		ssid 3587	. . . 4 ⊢ ran 𝐹 ⊆ ran 𝐹
46		cores 5555	. . . 4 ⊢ (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹))
47	45, 46	ax-mp 5	. . 3 ⊢ ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺 ∘ 𝐹)
48		dmres 5339	. . . . . . . . 9 ⊢ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
49		f1ocnv 6062	. . . . . . . . . . . 12 ⊢ ((1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))
50		f1odm 6054	. . . . . . . . . . . 12 ⊢ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}) → dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = (𝐵 ∖ ran 𝐹))
51	10, 49, 50	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) = (𝐵 ∖ ran 𝐹))
52	51	ineq2d 3776	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
53	52, 16	syl6eq 2660	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (ran 𝐹 ∩ dom ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = ∅)
54	48, 53	syl5eq 2656	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
55		relres 5346	. . . . . . . . 9 ⊢ Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)
56		reldm0 5264	. . . . . . . . 9 ⊢ (Rel (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) → ((^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅))
57	55, 56	ax-mp 5	. . . . . . . 8 ⊢ ((^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
58	54, 57	sylibr 223	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹) = ∅)
59	58	uneq2d 3729	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ ∅))
60		cnvun 5457	. . . . . . . . 9 ⊢ ^◡(𝐹 ∪ (1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
61	33, 60	eqtri 2632	. . . . . . . 8 ⊢ 𝐺 = (^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})))
62	61	reseq1i 5313	. . . . . . 7 ⊢ (𝐺 ↾ ran 𝐹) = ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹)
63		resundir 5331	. . . . . . 7 ⊢ ((^◡𝐹 ∪ ^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ↾ ran 𝐹) = ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
64		df-rn 5049	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
65	64	reseq2i 5314	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ ran 𝐹) = (^◡𝐹 ↾ dom ^◡𝐹)
66		relcnv 5422	. . . . . . . . . 10 ⊢ Rel ^◡𝐹
67		resdm 5361	. . . . . . . . . 10 ⊢ (Rel ^◡𝐹 → (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹)
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ (^◡𝐹 ↾ dom ^◡𝐹) = ^◡𝐹
69	65, 68	eqtri 2632	. . . . . . . 8 ⊢ (^◡𝐹 ↾ ran 𝐹) = ^◡𝐹
70	69	uneq1i 3725	. . . . . . 7 ⊢ ((^◡𝐹 ↾ ran 𝐹) ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹))
71	62, 63, 70	3eqtrri 2637	. . . . . 6 ⊢ (^◡𝐹 ∪ (^◡(1^st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
72		un0 3919	. . . . . 6 ⊢ (^◡𝐹 ∪ ∅) = ^◡𝐹
73	59, 71, 72	3eqtr3g 2667	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ↾ ran 𝐹) = ^◡𝐹)
74	73	coeq1d 5205	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (^◡𝐹 ∘ 𝐹))
75		f1cocnv1 6079	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
76	75	3ad2ant1 1075	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
77	74, 76	eqtrd 2644	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
78	47, 77	syl5eqr 2658	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
79	42, 44, 78	3jca 1235	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 ∪ cuni 4372 class class class wbr 4583 I cid 4948 × cxp 5036 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 ↾ cres 5040 ∘ ccom 5042 Rel wrel 5043 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 1^st c1st 7057 ≈ cen 7838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-1st 7059 df-2nd 7060 df-en 7842

This theorem is referenced by: domssex2 8005 domssex 8006

W3C validator