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

Theorem domss2 8407
Description: A corollary of disjenex 8406. 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 𝐺 = (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
Assertion
Ref Expression
domss2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐴 ⊆ ran 𝐺 ∧ (𝐺𝐹) = ( I ↾ 𝐴)))

Proof of Theorem domss2
StepHypRef Expression
1 f1f1orn 6402 . . . . . . . 8 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
213ad2ant1 1124 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴1-1-onto→ran 𝐹)
3 simp2 1128 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴𝑉)
4 rnexg 7376 . . . . . . . . . 10 (𝐴𝑉 → ran 𝐴 ∈ V)
53, 4syl 17 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐴 ∈ V)
6 uniexg 7232 . . . . . . . . 9 (ran 𝐴 ∈ V → ran 𝐴 ∈ V)
7 pwexg 5090 . . . . . . . . 9 ( ran 𝐴 ∈ V → 𝒫 ran 𝐴 ∈ V)
85, 6, 73syl 18 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝒫 ran 𝐴 ∈ V)
9 1stconst 7546 . . . . . . . 8 (𝒫 ran 𝐴 ∈ V → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹))
108, 9syl 17 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹))
11 difexg 5045 . . . . . . . . . 10 (𝐵𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12113ad2ant3 1126 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13 disjen 8405 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
143, 12, 13syl2anc 579 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
1514simpld 490 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅)
16 disjdif 4263 . . . . . . . 8 (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
1716a1i 11 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18 f1oun 6410 . . . . . . 7 (((𝐹:𝐴1-1-onto→ran 𝐹 ∧ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹)) ∧ ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
192, 10, 15, 17, 18syl22anc 829 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20 undif2 4267 . . . . . . . 8 (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹𝐵)
21 f1f 6351 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
22213ad2ant1 1124 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴𝐵)
2322frnd 6298 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐹𝐵)
24 ssequn1 4005 . . . . . . . . 9 (ran 𝐹𝐵 ↔ (ran 𝐹𝐵) = 𝐵)
2523, 24sylib 210 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹𝐵) = 𝐵)
2620, 25syl5eq 2825 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
2726f1oeq3d 6388 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵))
2819, 27mpbid 224 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵)
29 f1ocnv 6403 . . . . 5 ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵(𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3028, 29syl 17 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
31 domss2.1 . . . . 5 𝐺 = (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
32 f1oeq1 6380 . . . . 5 (𝐺 = (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) → (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
3331, 32ax-mp 5 . . . 4 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3430, 33sylibr 226 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
35 f1ofo 6398 . . . . 5 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → 𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
36 forn 6369 . . . . 5 (𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3734, 35, 363syl 18 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3837f1oeq3d 6388 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
3934, 38mpbird 249 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→ran 𝐺)
40 ssun1 3998 . . 3 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
4140, 37syl5sseqr 3872 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴 ⊆ ran 𝐺)
42 ssid 3841 . . . 4 ran 𝐹 ⊆ ran 𝐹
43 cores 5892 . . . 4 (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹))
4442, 43ax-mp 5 . . 3 ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹)
45 dmres 5668 . . . . . . . . 9 dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
46 f1ocnv 6403 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
47 f1odm 6395 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) → dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = (𝐵 ∖ ran 𝐹))
4810, 46, 473syl 18 . . . . . . . . . . 11 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = (𝐵 ∖ ran 𝐹))
4948ineq2d 4036 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
5049, 16syl6eq 2829 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = ∅)
5145, 50syl5eq 2825 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
52 relres 5675 . . . . . . . . 9 Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)
53 reldm0 5588 . . . . . . . . 9 (Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) → (((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅))
5452, 53ax-mp 5 . . . . . . . 8 (((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5551, 54sylibr 226 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5655uneq2d 3989 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ∅))
57 cnvun 5792 . . . . . . . . 9 (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5831, 57eqtri 2801 . . . . . . . 8 𝐺 = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5958reseq1i 5638 . . . . . . 7 (𝐺 ↾ ran 𝐹) = ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹)
60 resundir 5661 . . . . . . 7 ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹) = ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
61 df-rn 5366 . . . . . . . . . 10 ran 𝐹 = dom 𝐹
6261reseq2i 5639 . . . . . . . . 9 (𝐹 ↾ ran 𝐹) = (𝐹 ↾ dom 𝐹)
63 relcnv 5757 . . . . . . . . . 10 Rel 𝐹
64 resdm 5691 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
6563, 64ax-mp 5 . . . . . . . . 9 (𝐹 ↾ dom 𝐹) = 𝐹
6662, 65eqtri 2801 . . . . . . . 8 (𝐹 ↾ ran 𝐹) = 𝐹
6766uneq1i 3985 . . . . . . 7 ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
6859, 60, 673eqtrri 2806 . . . . . 6 (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69 un0 4192 . . . . . 6 (𝐹 ∪ ∅) = 𝐹
7056, 68, 693eqtr3g 2836 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺 ↾ ran 𝐹) = 𝐹)
7170coeq1d 5529 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐹𝐹))
72 f1cocnv1 6420 . . . . 5 (𝐹:𝐴1-1𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
73723ad2ant1 1124 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹𝐹) = ( I ↾ 𝐴))
7471, 73eqtrd 2813 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
7544, 74syl5eqr 2827 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺𝐹) = ( I ↾ 𝐴))
7639, 41, 753jca 1119 1 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐴 ⊆ ran 𝐺 ∧ (𝐺𝐹) = ( I ↾ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2106  Vcvv 3397  cdif 3788  cun 3789  cin 3790  wss 3791  c0 4140  𝒫 cpw 4378  {csn 4397   cuni 4671   class class class wbr 4886   I cid 5260   × cxp 5353  ccnv 5354  dom cdm 5355  ran crn 5356  cres 5357  ccom 5359  Rel wrel 5360  wf 6131  1-1wf1 6132  ontowfo 6133  1-1-ontowf1o 6134  1st c1st 7443  cen 8238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-1st 7445  df-2nd 7446  df-en 8242
This theorem is referenced by:  domssex2  8408  domssex  8409
  Copyright terms: Public domain W3C validator