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

Theorem hashfacen 14493
Description: The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by AV, 7-Aug-2024.)
Assertion
Ref Expression
hashfacen ((𝐴𝐵𝐶𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ≈ {𝑓𝑓:𝐵1-1-onto𝐷})
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝐶,𝑓   𝐷,𝑓

Proof of Theorem hashfacen
Dummy variables 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 8995 . 2 (𝐴𝐵 ↔ ∃𝑔 𝑔:𝐴1-1-onto𝐵)
2 bren 8995 . 2 (𝐶𝐷 ↔ ∃ :𝐶1-1-onto𝐷)
3 exdistrv 1955 . . 3 (∃𝑔(𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ↔ (∃𝑔 𝑔:𝐴1-1-onto𝐵 ∧ ∃ :𝐶1-1-onto𝐷))
4 f1osetex 8899 . . . . . 6 {𝑓𝑓:𝐴1-1-onto𝐶} ∈ V
54a1i 11 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ∈ V)
6 f1osetex 8899 . . . . . 6 {𝑓𝑓:𝐵1-1-onto𝐷} ∈ V
76a1i 11 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐵1-1-onto𝐷} ∈ V)
8 f1oco 6871 . . . . . . . . 9 ((:𝐶1-1-onto𝐷𝑥:𝐴1-1-onto𝐶) → (𝑥):𝐴1-1-onto𝐷)
98adantll 714 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑥:𝐴1-1-onto𝐶) → (𝑥):𝐴1-1-onto𝐷)
10 f1ocnv 6860 . . . . . . . . 9 (𝑔:𝐴1-1-onto𝐵𝑔:𝐵1-1-onto𝐴)
1110ad2antrr 726 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑥:𝐴1-1-onto𝐶) → 𝑔:𝐵1-1-onto𝐴)
12 f1oco 6871 . . . . . . . 8 (((𝑥):𝐴1-1-onto𝐷𝑔:𝐵1-1-onto𝐴) → ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷)
139, 11, 12syl2anc 584 . . . . . . 7 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑥:𝐴1-1-onto𝐶) → ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷)
1413ex 412 . . . . . 6 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → (𝑥:𝐴1-1-onto𝐶 → ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷))
15 vex 3484 . . . . . . 7 𝑥 ∈ V
16 f1oeq1 6836 . . . . . . 7 (𝑓 = 𝑥 → (𝑓:𝐴1-1-onto𝐶𝑥:𝐴1-1-onto𝐶))
1715, 16elab 3679 . . . . . 6 (𝑥 ∈ {𝑓𝑓:𝐴1-1-onto𝐶} ↔ 𝑥:𝐴1-1-onto𝐶)
18 vex 3484 . . . . . . . . 9 ∈ V
1918, 15coex 7952 . . . . . . . 8 (𝑥) ∈ V
20 vex 3484 . . . . . . . . 9 𝑔 ∈ V
2120cnvex 7947 . . . . . . . 8 𝑔 ∈ V
2219, 21coex 7952 . . . . . . 7 ((𝑥) ∘ 𝑔) ∈ V
23 f1oeq1 6836 . . . . . . 7 (𝑓 = ((𝑥) ∘ 𝑔) → (𝑓:𝐵1-1-onto𝐷 ↔ ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷))
2422, 23elab 3679 . . . . . 6 (((𝑥) ∘ 𝑔) ∈ {𝑓𝑓:𝐵1-1-onto𝐷} ↔ ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷)
2514, 17, 243imtr4g 296 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → (𝑥 ∈ {𝑓𝑓:𝐴1-1-onto𝐶} → ((𝑥) ∘ 𝑔) ∈ {𝑓𝑓:𝐵1-1-onto𝐷}))
26 f1ocnv 6860 . . . . . . . . 9 (:𝐶1-1-onto𝐷:𝐷1-1-onto𝐶)
2726ad2antlr 727 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑦:𝐵1-1-onto𝐷) → :𝐷1-1-onto𝐶)
28 f1oco 6871 . . . . . . . . . 10 ((𝑦:𝐵1-1-onto𝐷𝑔:𝐴1-1-onto𝐵) → (𝑦𝑔):𝐴1-1-onto𝐷)
2928ancoms 458 . . . . . . . . 9 ((𝑔:𝐴1-1-onto𝐵𝑦:𝐵1-1-onto𝐷) → (𝑦𝑔):𝐴1-1-onto𝐷)
3029adantlr 715 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑦:𝐵1-1-onto𝐷) → (𝑦𝑔):𝐴1-1-onto𝐷)
31 f1oco 6871 . . . . . . . 8 ((:𝐷1-1-onto𝐶 ∧ (𝑦𝑔):𝐴1-1-onto𝐷) → ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶)
3227, 30, 31syl2anc 584 . . . . . . 7 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑦:𝐵1-1-onto𝐷) → ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶)
3332ex 412 . . . . . 6 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → (𝑦:𝐵1-1-onto𝐷 → ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶))
34 vex 3484 . . . . . . 7 𝑦 ∈ V
35 f1oeq1 6836 . . . . . . 7 (𝑓 = 𝑦 → (𝑓:𝐵1-1-onto𝐷𝑦:𝐵1-1-onto𝐷))
3634, 35elab 3679 . . . . . 6 (𝑦 ∈ {𝑓𝑓:𝐵1-1-onto𝐷} ↔ 𝑦:𝐵1-1-onto𝐷)
3718cnvex 7947 . . . . . . . 8 ∈ V
3834, 20coex 7952 . . . . . . . 8 (𝑦𝑔) ∈ V
3937, 38coex 7952 . . . . . . 7 ( ∘ (𝑦𝑔)) ∈ V
40 f1oeq1 6836 . . . . . . 7 (𝑓 = ( ∘ (𝑦𝑔)) → (𝑓:𝐴1-1-onto𝐶 ↔ ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶))
4139, 40elab 3679 . . . . . 6 (( ∘ (𝑦𝑔)) ∈ {𝑓𝑓:𝐴1-1-onto𝐶} ↔ ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶)
4233, 36, 413imtr4g 296 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → (𝑦 ∈ {𝑓𝑓:𝐵1-1-onto𝐷} → ( ∘ (𝑦𝑔)) ∈ {𝑓𝑓:𝐴1-1-onto𝐶}))
4317, 36anbi12i 628 . . . . . 6 ((𝑥 ∈ {𝑓𝑓:𝐴1-1-onto𝐶} ∧ 𝑦 ∈ {𝑓𝑓:𝐵1-1-onto𝐷}) ↔ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷))
44 coass 6285 . . . . . . . . . . 11 (((𝑥) ∘ 𝑔) ∘ 𝑔) = ((𝑥) ∘ (𝑔𝑔))
45 f1ococnv1 6877 . . . . . . . . . . . . . 14 (𝑔:𝐴1-1-onto𝐵 → (𝑔𝑔) = ( I ↾ 𝐴))
4645ad2antrr 726 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑔𝑔) = ( I ↾ 𝐴))
4746coeq2d 5873 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ (𝑔𝑔)) = ((𝑥) ∘ ( I ↾ 𝐴)))
489adantrr 717 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑥):𝐴1-1-onto𝐷)
49 f1of 6848 . . . . . . . . . . . . 13 ((𝑥):𝐴1-1-onto𝐷 → (𝑥):𝐴𝐷)
50 fcoi1 6782 . . . . . . . . . . . . 13 ((𝑥):𝐴𝐷 → ((𝑥) ∘ ( I ↾ 𝐴)) = (𝑥))
5148, 49, 503syl 18 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ ( I ↾ 𝐴)) = (𝑥))
5247, 51eqtrd 2777 . . . . . . . . . . 11 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ (𝑔𝑔)) = (𝑥))
5344, 52eqtr2id 2790 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑥) = (((𝑥) ∘ 𝑔) ∘ 𝑔))
54 coass 6285 . . . . . . . . . . 11 (() ∘ (𝑦𝑔)) = ( ∘ ( ∘ (𝑦𝑔)))
55 f1ococnv2 6875 . . . . . . . . . . . . . 14 (:𝐶1-1-onto𝐷 → () = ( I ↾ 𝐷))
5655ad2antlr 727 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → () = ( I ↾ 𝐷))
5756coeq1d 5872 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (() ∘ (𝑦𝑔)) = (( I ↾ 𝐷) ∘ (𝑦𝑔)))
5830adantrl 716 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑦𝑔):𝐴1-1-onto𝐷)
59 f1of 6848 . . . . . . . . . . . . 13 ((𝑦𝑔):𝐴1-1-onto𝐷 → (𝑦𝑔):𝐴𝐷)
60 fcoi2 6783 . . . . . . . . . . . . 13 ((𝑦𝑔):𝐴𝐷 → (( I ↾ 𝐷) ∘ (𝑦𝑔)) = (𝑦𝑔))
6158, 59, 603syl 18 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (( I ↾ 𝐷) ∘ (𝑦𝑔)) = (𝑦𝑔))
6257, 61eqtrd 2777 . . . . . . . . . . 11 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (() ∘ (𝑦𝑔)) = (𝑦𝑔))
6354, 62eqtr3id 2791 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ( ∘ ( ∘ (𝑦𝑔))) = (𝑦𝑔))
6453, 63eqeq12d 2753 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ (((𝑥) ∘ 𝑔) ∘ 𝑔) = (𝑦𝑔)))
65 eqcom 2744 . . . . . . . . 9 ((((𝑥) ∘ 𝑔) ∘ 𝑔) = (𝑦𝑔) ↔ (𝑦𝑔) = (((𝑥) ∘ 𝑔) ∘ 𝑔))
6664, 65bitrdi 287 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ (𝑦𝑔) = (((𝑥) ∘ 𝑔) ∘ 𝑔)))
67 f1of1 6847 . . . . . . . . . 10 (:𝐶1-1-onto𝐷:𝐶1-1𝐷)
6867ad2antlr 727 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → :𝐶1-1𝐷)
69 f1of 6848 . . . . . . . . . 10 (𝑥:𝐴1-1-onto𝐶𝑥:𝐴𝐶)
7069ad2antrl 728 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → 𝑥:𝐴𝐶)
7132adantrl 716 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶)
72 f1of 6848 . . . . . . . . . 10 (( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶 → ( ∘ (𝑦𝑔)):𝐴𝐶)
7371, 72syl 17 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ( ∘ (𝑦𝑔)):𝐴𝐶)
74 cocan1 7311 . . . . . . . . 9 ((:𝐶1-1𝐷𝑥:𝐴𝐶 ∧ ( ∘ (𝑦𝑔)):𝐴𝐶) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ 𝑥 = ( ∘ (𝑦𝑔))))
7568, 70, 73, 74syl3anc 1373 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ 𝑥 = ( ∘ (𝑦𝑔))))
76 f1ofo 6855 . . . . . . . . . 10 (𝑔:𝐴1-1-onto𝐵𝑔:𝐴onto𝐵)
7776ad2antrr 726 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → 𝑔:𝐴onto𝐵)
78 f1ofn 6849 . . . . . . . . . 10 (𝑦:𝐵1-1-onto𝐷𝑦 Fn 𝐵)
7978ad2antll 729 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → 𝑦 Fn 𝐵)
8013adantrr 717 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷)
81 f1ofn 6849 . . . . . . . . . 10 (((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷 → ((𝑥) ∘ 𝑔) Fn 𝐵)
8280, 81syl 17 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ 𝑔) Fn 𝐵)
83 cocan2 7312 . . . . . . . . 9 ((𝑔:𝐴onto𝐵𝑦 Fn 𝐵 ∧ ((𝑥) ∘ 𝑔) Fn 𝐵) → ((𝑦𝑔) = (((𝑥) ∘ 𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑥) ∘ 𝑔)))
8477, 79, 82, 83syl3anc 1373 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑦𝑔) = (((𝑥) ∘ 𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑥) ∘ 𝑔)))
8566, 75, 843bitr3d 309 . . . . . . 7 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑥 = ( ∘ (𝑦𝑔)) ↔ 𝑦 = ((𝑥) ∘ 𝑔)))
8685ex 412 . . . . . 6 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → ((𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷) → (𝑥 = ( ∘ (𝑦𝑔)) ↔ 𝑦 = ((𝑥) ∘ 𝑔))))
8743, 86biimtrid 242 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → ((𝑥 ∈ {𝑓𝑓:𝐴1-1-onto𝐶} ∧ 𝑦 ∈ {𝑓𝑓:𝐵1-1-onto𝐷}) → (𝑥 = ( ∘ (𝑦𝑔)) ↔ 𝑦 = ((𝑥) ∘ 𝑔))))
885, 7, 25, 42, 87en3d 9029 . . . 4 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ≈ {𝑓𝑓:𝐵1-1-onto𝐷})
8988exlimivv 1932 . . 3 (∃𝑔(𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ≈ {𝑓𝑓:𝐵1-1-onto𝐷})
903, 89sylbir 235 . 2 ((∃𝑔 𝑔:𝐴1-1-onto𝐵 ∧ ∃ :𝐶1-1-onto𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ≈ {𝑓𝑓:𝐵1-1-onto𝐷})
911, 2, 90syl2anb 598 1 ((𝐴𝐵𝐶𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ≈ {𝑓𝑓:𝐵1-1-onto𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  Vcvv 3480   class class class wbr 5143   I cid 5577  ccnv 5684  cres 5687  ccom 5689   Fn wfn 6556  wf 6557  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560  cen 8982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-en 8986
This theorem is referenced by:  poimirlem9  37636
  Copyright terms: Public domain W3C validator