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

Theorem domss2 9131
Description: A corollary of disjenex 9130. 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 6834 . . . . . . . 8 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
213ad2ant1 1130 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴1-1-onto→ran 𝐹)
3 simp2 1134 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴𝑉)
4 rnexg 7888 . . . . . . . . . 10 (𝐴𝑉 → ran 𝐴 ∈ V)
53, 4syl 17 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐴 ∈ V)
6 uniexg 7723 . . . . . . . . 9 (ran 𝐴 ∈ V → ran 𝐴 ∈ V)
7 pwexg 5366 . . . . . . . . 9 ( ran 𝐴 ∈ V → 𝒫 ran 𝐴 ∈ V)
85, 6, 73syl 18 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝒫 ran 𝐴 ∈ V)
9 1stconst 8080 . . . . . . . 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 5317 . . . . . . . . . 10 (𝐵𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12113ad2ant3 1132 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13 disjen 9129 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
143, 12, 13syl2anc 583 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
1514simpld 494 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅)
16 disjdif 4463 . . . . . . . 8 (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
1716a1i 11 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18 f1oun 6842 . . . . . . 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 836 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20 undif2 4468 . . . . . . . 8 (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹𝐵)
21 f1f 6777 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
22213ad2ant1 1130 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴𝐵)
2322frnd 6715 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐹𝐵)
24 ssequn1 4172 . . . . . . . . 9 (ran 𝐹𝐵 ↔ (ran 𝐹𝐵) = 𝐵)
2523, 24sylib 217 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹𝐵) = 𝐵)
2620, 25eqtrid 2776 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
2726f1oeq3d 6820 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵))
2819, 27mpbid 231 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵)
29 f1ocnv 6835 . . . . 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 6811 . . . . 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 233 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
35 f1ofo 6830 . . . . 5 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → 𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
36 forn 6798 . . . . 5 (𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3734, 35, 363syl 18 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3837f1oeq3d 6820 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
3934, 38mpbird 257 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→ran 𝐺)
40 ssun1 4164 . . 3 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
4140, 37sseqtrrid 4027 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴 ⊆ ran 𝐺)
42 ssid 3996 . . . 4 ran 𝐹 ⊆ ran 𝐹
43 cores 6238 . . . 4 (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹))
4442, 43ax-mp 5 . . 3 ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹)
45 dmres 5993 . . . . . . . . 9 dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
46 f1ocnv 6835 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
47 f1odm 6827 . . . . . . . . . . . 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 4204 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
5049, 16eqtrdi 2780 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = ∅)
5145, 50eqtrid 2776 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
52 relres 6000 . . . . . . . . 9 Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)
53 reldm0 5917 . . . . . . . . 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 233 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5655uneq2d 4155 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ∅))
57 cnvun 6132 . . . . . . . . 9 (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5831, 57eqtri 2752 . . . . . . . 8 𝐺 = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5958reseq1i 5967 . . . . . . 7 (𝐺 ↾ ran 𝐹) = ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹)
60 resundir 5986 . . . . . . 7 ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹) = ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
61 df-rn 5677 . . . . . . . . . 10 ran 𝐹 = dom 𝐹
6261reseq2i 5968 . . . . . . . . 9 (𝐹 ↾ ran 𝐹) = (𝐹 ↾ dom 𝐹)
63 relcnv 6093 . . . . . . . . . 10 Rel 𝐹
64 resdm 6016 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
6563, 64ax-mp 5 . . . . . . . . 9 (𝐹 ↾ dom 𝐹) = 𝐹
6662, 65eqtri 2752 . . . . . . . 8 (𝐹 ↾ ran 𝐹) = 𝐹
6766uneq1i 4151 . . . . . . 7 ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
6859, 60, 673eqtrri 2757 . . . . . 6 (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69 un0 4382 . . . . . 6 (𝐹 ∪ ∅) = 𝐹
7056, 68, 693eqtr3g 2787 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺 ↾ ran 𝐹) = 𝐹)
7170coeq1d 5851 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐹𝐹))
72 f1cocnv1 6853 . . . . 5 (𝐹:𝐴1-1𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
73723ad2ant1 1130 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹𝐹) = ( I ↾ 𝐴))
7471, 73eqtrd 2764 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
7544, 74eqtr3id 2778 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺𝐹) = ( I ↾ 𝐴))
7639, 41, 753jca 1125 1 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐴 ⊆ ran 𝐺 ∧ (𝐺𝐹) = ( I ↾ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  Vcvv 3466  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4314  𝒫 cpw 4594  {csn 4620   cuni 4899   class class class wbr 5138   I cid 5563   × cxp 5664  ccnv 5665  dom cdm 5666  ran crn 5667  cres 5668  ccom 5670  Rel wrel 5671  wf 6529  1-1wf1 6530  ontowfo 6531  1-1-ontowf1o 6532  1st c1st 7966  cen 8931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-1st 7968  df-2nd 7969  df-en 8935
This theorem is referenced by:  domssex2  9132  domssex  9133
  Copyright terms: Public domain W3C validator