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

Theorem domss2 8670
Description: A corollary of disjenex 8669. 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 6621 . . . . . . . 8 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
213ad2ant1 1129 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴1-1-onto→ran 𝐹)
3 simp2 1133 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴𝑉)
4 rnexg 7608 . . . . . . . . . 10 (𝐴𝑉 → ran 𝐴 ∈ V)
53, 4syl 17 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐴 ∈ V)
6 uniexg 7460 . . . . . . . . 9 (ran 𝐴 ∈ V → ran 𝐴 ∈ V)
7 pwexg 5272 . . . . . . . . 9 ( ran 𝐴 ∈ V → 𝒫 ran 𝐴 ∈ V)
85, 6, 73syl 18 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝒫 ran 𝐴 ∈ V)
9 1stconst 7789 . . . . . . . 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 5224 . . . . . . . . . 10 (𝐵𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12113ad2ant3 1131 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13 disjen 8668 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
143, 12, 13syl2anc 586 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
1514simpld 497 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅)
16 disjdif 4421 . . . . . . . 8 (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
1716a1i 11 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18 f1oun 6629 . . . . . . 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 4425 . . . . . . . 8 (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹𝐵)
21 f1f 6570 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
22213ad2ant1 1129 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴𝐵)
2322frnd 6516 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐹𝐵)
24 ssequn1 4156 . . . . . . . . 9 (ran 𝐹𝐵 ↔ (ran 𝐹𝐵) = 𝐵)
2523, 24sylib 220 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹𝐵) = 𝐵)
2620, 25syl5eq 2868 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
2726f1oeq3d 6607 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵))
2819, 27mpbid 234 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵)
29 f1ocnv 6622 . . . . 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 6599 . . . . 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 236 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
35 f1ofo 6617 . . . . 5 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → 𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
36 forn 6588 . . . . 5 (𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3734, 35, 363syl 18 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3837f1oeq3d 6607 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
3934, 38mpbird 259 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→ran 𝐺)
40 ssun1 4148 . . 3 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
4140, 37sseqtrrid 4020 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴 ⊆ ran 𝐺)
42 ssid 3989 . . . 4 ran 𝐹 ⊆ ran 𝐹
43 cores 6097 . . . 4 (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹))
4442, 43ax-mp 5 . . 3 ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹)
45 dmres 5870 . . . . . . . . 9 dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
46 f1ocnv 6622 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
47 f1odm 6614 . . . . . . . . . . . 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 4189 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
5049, 16syl6eq 2872 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = ∅)
5145, 50syl5eq 2868 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
52 relres 5877 . . . . . . . . 9 Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)
53 reldm0 5793 . . . . . . . . 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 236 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5655uneq2d 4139 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ∅))
57 cnvun 5996 . . . . . . . . 9 (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5831, 57eqtri 2844 . . . . . . . 8 𝐺 = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5958reseq1i 5844 . . . . . . 7 (𝐺 ↾ ran 𝐹) = ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹)
60 resundir 5863 . . . . . . 7 ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹) = ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
61 df-rn 5561 . . . . . . . . . 10 ran 𝐹 = dom 𝐹
6261reseq2i 5845 . . . . . . . . 9 (𝐹 ↾ ran 𝐹) = (𝐹 ↾ dom 𝐹)
63 relcnv 5962 . . . . . . . . . 10 Rel 𝐹
64 resdm 5892 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
6563, 64ax-mp 5 . . . . . . . . 9 (𝐹 ↾ dom 𝐹) = 𝐹
6662, 65eqtri 2844 . . . . . . . 8 (𝐹 ↾ ran 𝐹) = 𝐹
6766uneq1i 4135 . . . . . . 7 ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
6859, 60, 673eqtrri 2849 . . . . . 6 (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69 un0 4344 . . . . . 6 (𝐹 ∪ ∅) = 𝐹
7056, 68, 693eqtr3g 2879 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺 ↾ ran 𝐹) = 𝐹)
7170coeq1d 5727 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐹𝐹))
72 f1cocnv1 6639 . . . . 5 (𝐹:𝐴1-1𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
73723ad2ant1 1129 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹𝐹) = ( I ↾ 𝐴))
7471, 73eqtrd 2856 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
7544, 74syl5eqr 2870 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺𝐹) = ( I ↾ 𝐴))
7639, 41, 753jca 1124 1 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐴 ⊆ ran 𝐺 ∧ (𝐺𝐹) = ( I ↾ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083   = wceq 1533  wcel 2110  Vcvv 3495  cdif 3933  cun 3934  cin 3935  wss 3936  c0 4291  𝒫 cpw 4539  {csn 4561   cuni 4832   class class class wbr 5059   I cid 5454   × cxp 5548  ccnv 5549  dom cdm 5550  ran crn 5551  cres 5552  ccom 5554  Rel wrel 5555  wf 6346  1-1wf1 6347  ontowfo 6348  1-1-ontowf1o 6349  1st c1st 7681  cen 8500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-1st 7683  df-2nd 7684  df-en 8504
This theorem is referenced by:  domssex2  8671  domssex  8672
  Copyright terms: Public domain W3C validator