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

Theorem domss2 8272
Description: A corollary of disjenex 8271. 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 6297 . . . . . . . 8 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
213ad2ant1 1125 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴1-1-onto→ran 𝐹)
3 simp2 1129 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴𝑉)
4 rnexg 7251 . . . . . . . . . 10 (𝐴𝑉 → ran 𝐴 ∈ V)
53, 4syl 17 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐴 ∈ V)
6 uniexg 7108 . . . . . . . . 9 (ran 𝐴 ∈ V → ran 𝐴 ∈ V)
7 pwexg 4987 . . . . . . . . 9 ( ran 𝐴 ∈ V → 𝒫 ran 𝐴 ∈ V)
85, 6, 73syl 18 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝒫 ran 𝐴 ∈ V)
9 1stconst 7421 . . . . . . . 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 4948 . . . . . . . . . 10 (𝐵𝑊 → (𝐵 ∖ ran 𝐹) ∈ V)
12113ad2ant3 1127 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐵 ∖ ran 𝐹) ∈ V)
13 disjen 8270 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐵 ∖ ran 𝐹) ∈ V) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
143, 12, 13syl2anc 696 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅ ∧ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) ≈ (𝐵 ∖ ran 𝐹)))
1514simpld 477 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐴 ∩ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = ∅)
16 disjdif 4172 . . . . . . . 8 (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅
1716a1i 11 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)) = ∅)
18 f1oun 6305 . . . . . . 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 1464 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)))
20 undif2 4176 . . . . . . . 8 (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = (ran 𝐹𝐵)
21 f1f 6250 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
22213ad2ant1 1125 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐹:𝐴𝐵)
23 frn 6202 . . . . . . . . . 10 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
2422, 23syl 17 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐹𝐵)
25 ssequn1 3914 . . . . . . . . 9 (ran 𝐹𝐵 ↔ (ran 𝐹𝐵) = 𝐵)
2624, 25sylib 208 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹𝐵) = 𝐵)
2720, 26syl5eq 2794 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵)
28 f1oeq3 6278 . . . . . . 7 ((ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) = 𝐵 → ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵))
2927, 28syl 17 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto→(ran 𝐹 ∪ (𝐵 ∖ ran 𝐹)) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵))
3019, 29mpbid 222 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵)
31 f1ocnv 6298 . . . . 5 ((𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))–1-1-onto𝐵(𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3230, 31syl 17 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
33 domss2.1 . . . . 5 𝐺 = (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
34 f1oeq1 6276 . . . . 5 (𝐺 = (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) → (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
3533, 34ax-mp 5 . . . 4 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↔ (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))):𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3632, 35sylibr 224 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
37 f1ofo 6293 . . . . 5 (𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → 𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
38 forn 6267 . . . . 5 (𝐺:𝐵onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
3936, 37, 383syl 18 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
40 f1oeq3 6278 . . . 4 (ran 𝐺 = (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) → (𝐺:𝐵1-1-onto→ran 𝐺𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
4139, 40syl 17 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐺:𝐵1-1-onto→(𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))))
4236, 41mpbird 247 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐺:𝐵1-1-onto→ran 𝐺)
43 ssun1 3907 . . 3 𝐴 ⊆ (𝐴 ∪ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
4443, 39syl5sseqr 3783 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → 𝐴 ⊆ ran 𝐺)
45 ssid 3753 . . . 4 ran 𝐹 ⊆ ran 𝐹
46 cores 5787 . . . 4 (ran 𝐹 ⊆ ran 𝐹 → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹))
4745, 46ax-mp 5 . . 3 ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐺𝐹)
48 dmres 5565 . . . . . . . . 9 dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
49 f1ocnv 6298 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})–1-1-onto→(𝐵 ∖ ran 𝐹) → (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))
50 f1odm 6290 . . . . . . . . . . . 12 ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})):(𝐵 ∖ ran 𝐹)–1-1-onto→((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}) → dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = (𝐵 ∖ ran 𝐹))
5110, 49, 503syl 18 . . . . . . . . . . 11 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) = (𝐵 ∖ ran 𝐹))
5251ineq2d 3945 . . . . . . . . . 10 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (ran 𝐹 ∩ (𝐵 ∖ ran 𝐹)))
5352, 16syl6eq 2798 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (ran 𝐹 ∩ dom (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = ∅)
5448, 53syl5eq 2794 . . . . . . . 8 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
55 relres 5572 . . . . . . . . 9 Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)
56 reldm0 5486 . . . . . . . . 9 (Rel ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) → (((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅))
5755, 56ax-mp 5 . . . . . . . 8 (((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅ ↔ dom ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5854, 57sylibr 224 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹) = ∅)
5958uneq2d 3898 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ∅))
60 cnvun 5684 . . . . . . . . 9 (𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
6133, 60eqtri 2770 . . . . . . . 8 𝐺 = (𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})))
6261reseq1i 5535 . . . . . . 7 (𝐺 ↾ ran 𝐹) = ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹)
63 resundir 5557 . . . . . . 7 ((𝐹(1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴}))) ↾ ran 𝐹) = ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
64 df-rn 5265 . . . . . . . . . 10 ran 𝐹 = dom 𝐹
6564reseq2i 5536 . . . . . . . . 9 (𝐹 ↾ ran 𝐹) = (𝐹 ↾ dom 𝐹)
66 relcnv 5649 . . . . . . . . . 10 Rel 𝐹
67 resdm 5587 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
6866, 67ax-mp 5 . . . . . . . . 9 (𝐹 ↾ dom 𝐹) = 𝐹
6965, 68eqtri 2770 . . . . . . . 8 (𝐹 ↾ ran 𝐹) = 𝐹
7069uneq1i 3894 . . . . . . 7 ((𝐹 ↾ ran 𝐹) ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹))
7162, 63, 703eqtrri 2775 . . . . . 6 (𝐹 ∪ ((1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ran 𝐴})) ↾ ran 𝐹)) = (𝐺 ↾ ran 𝐹)
72 un0 4098 . . . . . 6 (𝐹 ∪ ∅) = 𝐹
7359, 71, 723eqtr3g 2805 . . . . 5 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺 ↾ ran 𝐹) = 𝐹)
7473coeq1d 5427 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = (𝐹𝐹))
75 f1cocnv1 6315 . . . . 5 (𝐹:𝐴1-1𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
76753ad2ant1 1125 . . . 4 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐹𝐹) = ( I ↾ 𝐴))
7774, 76eqtrd 2782 . . 3 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → ((𝐺 ↾ ran 𝐹) ∘ 𝐹) = ( I ↾ 𝐴))
7847, 77syl5eqr 2796 . 2 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺𝐹) = ( I ↾ 𝐴))
7942, 44, 783jca 1403 1 ((𝐹:𝐴1-1𝐵𝐴𝑉𝐵𝑊) → (𝐺:𝐵1-1-onto→ran 𝐺𝐴 ⊆ ran 𝐺 ∧ (𝐺𝐹) = ( I ↾ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1620  wcel 2127  Vcvv 3328  cdif 3700  cun 3701  cin 3702  wss 3703  c0 4046  𝒫 cpw 4290  {csn 4309   cuni 4576   class class class wbr 4792   I cid 5161   × cxp 5252  ccnv 5253  dom cdm 5254  ran crn 5255  cres 5256  ccom 5258  Rel wrel 5259  wf 6033  1-1wf1 6034  ontowfo 6035  1-1-ontowf1o 6036  1st c1st 7319  cen 8106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-1st 7321  df-2nd 7322  df-en 8110
This theorem is referenced by:  domssex2  8273  domssex  8274
  Copyright terms: Public domain W3C validator