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

Theorem domss2 8698
 Description: A corollary of disjenex 8697. 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 6613 . . . . . . . 8 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
213ad2ant1 1130 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴1-1-onto→ran 𝐹)
3 simp2 1134 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴𝑉)
4 rnexg 7614 . . . . . . . . . 10 (𝐴𝑉 → ran 𝐴 ∈ V)
53, 4syl 17 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐴 ∈ V)
6 uniexg 7464 . . . . . . . . 9 (ran 𝐴 ∈ V → ran 𝐴 ∈ V)
7 pwexg 5247 . . . . . . . . 9 ( ran 𝐴 ∈ V → 𝒫 ran 𝐴 ∈ V)
85, 6, 73syl 18 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝒫 ran 𝐴 ∈ V)
9 1stconst 7800 . . . . . . . 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 5197 . . . . . . . . . 10 (𝐵𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12113ad2ant3 1132 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13 disjen 8696 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
143, 12, 13syl2anc 587 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
1514simpld 498 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅)
16 disjdif 4368 . . . . . . . 8 (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
1716a1i 11 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18 f1oun 6621 . . . . . . 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 837 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20 undif2 4373 . . . . . . . 8 (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹𝐵)
21 f1f 6560 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
22213ad2ant1 1130 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴𝐵)
2322frnd 6505 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐹𝐵)
24 ssequn1 4085 . . . . . . . . 9 (ran 𝐹𝐵 ↔ (ran 𝐹𝐵) = 𝐵)
2523, 24sylib 221 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹𝐵) = 𝐵)
2620, 25syl5eq 2805 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
2726f1oeq3d 6599 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵))
2819, 27mpbid 235 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵)
29 f1ocnv 6614 . . . . 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 6590 . . . . 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 237 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
35 f1ofo 6609 . . . . 5 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → 𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
36 forn 6579 . . . . 5 (𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3734, 35, 363syl 18 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3837f1oeq3d 6599 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
3934, 38mpbird 260 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→ran 𝐺)
40 ssun1 4077 . . 3 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
4140, 37sseqtrrid 3945 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴 ⊆ ran 𝐺)
42 ssid 3914 . . . 4 ran 𝐹 ⊆ ran 𝐹
43 cores 6079 . . . 4 (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹))
4442, 43ax-mp 5 . . 3 ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹)
45 dmres 5845 . . . . . . . . 9 dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
46 f1ocnv 6614 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
47 f1odm 6606 . . . . . . . . . . . 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 4117 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
5049, 16eqtrdi 2809 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = ∅)
5145, 50syl5eq 2805 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
52 relres 5852 . . . . . . . . 9 Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)
53 reldm0 5769 . . . . . . . . 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 237 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5655uneq2d 4068 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ∅))
57 cnvun 5973 . . . . . . . . 9 (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5831, 57eqtri 2781 . . . . . . . 8 𝐺 = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
5958reseq1i 5819 . . . . . . 7 (𝐺 ↾ ran 𝐹) = ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹)
60 resundir 5838 . . . . . . 7 ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹) = ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
61 df-rn 5535 . . . . . . . . . 10 ran 𝐹 = dom 𝐹
6261reseq2i 5820 . . . . . . . . 9 (𝐹 ↾ ran 𝐹) = (𝐹 ↾ dom 𝐹)
63 relcnv 5939 . . . . . . . . . 10 Rel 𝐹
64 resdm 5868 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
6563, 64ax-mp 5 . . . . . . . . 9 (𝐹 ↾ dom 𝐹) = 𝐹
6662, 65eqtri 2781 . . . . . . . 8 (𝐹 ↾ ran 𝐹) = 𝐹
6766uneq1i 4064 . . . . . . 7 ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
6859, 60, 673eqtrri 2786 . . . . . 6 (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
69 un0 4286 . . . . . 6 (𝐹 ∪ ∅) = 𝐹
7056, 68, 693eqtr3g 2816 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺 ↾ ran 𝐹) = 𝐹)
7170coeq1d 5701 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐹𝐹))
72 f1cocnv1 6631 . . . . 5 (𝐹:𝐴1-1𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
73723ad2ant1 1130 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹𝐹) = ( I ↾ 𝐴))
7471, 73eqtrd 2793 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
7544, 74syl5eqr 2807 . 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 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  Vcvv 3409   ∖ cdif 3855   ∪ cun 3856   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  𝒫 cpw 4494  {csn 4522  ∪ cuni 4798   class class class wbr 5032   I cid 5429   × cxp 5522  ◡ccnv 5523  dom cdm 5524  ran crn 5525   ↾ cres 5526   ∘ ccom 5528  Rel wrel 5529  ⟶wf 6331  –1-1→wf1 6332  –onto→wfo 6333  –1-1-onto→wf1o 6334  1st c1st 7691   ≈ cen 8524 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-1st 7693  df-2nd 7694  df-en 8528 This theorem is referenced by:  domssex2  8699  domssex  8700
 Copyright terms: Public domain W3C validator