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

Theorem hashfacen 14490
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 8994 . 2 (𝐴𝐵 ↔ ∃𝑔 𝑔:𝐴1-1-onto𝐵)
2 bren 8994 . 2 (𝐶𝐷 ↔ ∃ :𝐶1-1-onto𝐷)
3 exdistrv 1953 . . 3 (∃𝑔(𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ↔ (∃𝑔 𝑔:𝐴1-1-onto𝐵 ∧ ∃ :𝐶1-1-onto𝐷))
4 f1osetex 8898 . . . . . 6 {𝑓𝑓:𝐴1-1-onto𝐶} ∈ V
54a1i 11 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ∈ V)
6 f1osetex 8898 . . . . . 6 {𝑓𝑓:𝐵1-1-onto𝐷} ∈ V
76a1i 11 . . . . 5 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐵1-1-onto𝐷} ∈ V)
8 f1oco 6872 . . . . . . . . 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 6861 . . . . . . . . 9 (𝑔:𝐴1-1-onto𝐵𝑔:𝐵1-1-onto𝐴)
1110ad2antrr 726 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑥:𝐴1-1-onto𝐶) → 𝑔:𝐵1-1-onto𝐴)
12 f1oco 6872 . . . . . . . 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 3482 . . . . . . 7 𝑥 ∈ V
16 f1oeq1 6837 . . . . . . 7 (𝑓 = 𝑥 → (𝑓:𝐴1-1-onto𝐶𝑥:𝐴1-1-onto𝐶))
1715, 16elab 3681 . . . . . 6 (𝑥 ∈ {𝑓𝑓:𝐴1-1-onto𝐶} ↔ 𝑥:𝐴1-1-onto𝐶)
18 vex 3482 . . . . . . . . 9 ∈ V
1918, 15coex 7953 . . . . . . . 8 (𝑥) ∈ V
20 vex 3482 . . . . . . . . 9 𝑔 ∈ V
2120cnvex 7948 . . . . . . . 8 𝑔 ∈ V
2219, 21coex 7953 . . . . . . 7 ((𝑥) ∘ 𝑔) ∈ V
23 f1oeq1 6837 . . . . . . 7 (𝑓 = ((𝑥) ∘ 𝑔) → (𝑓:𝐵1-1-onto𝐷 ↔ ((𝑥) ∘ 𝑔):𝐵1-1-onto𝐷))
2422, 23elab 3681 . . . . . 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 6861 . . . . . . . . 9 (:𝐶1-1-onto𝐷:𝐷1-1-onto𝐶)
2726ad2antlr 727 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ 𝑦:𝐵1-1-onto𝐷) → :𝐷1-1-onto𝐶)
28 f1oco 6872 . . . . . . . . . 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 6872 . . . . . . . 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 3482 . . . . . . 7 𝑦 ∈ V
35 f1oeq1 6837 . . . . . . 7 (𝑓 = 𝑦 → (𝑓:𝐵1-1-onto𝐷𝑦:𝐵1-1-onto𝐷))
3634, 35elab 3681 . . . . . 6 (𝑦 ∈ {𝑓𝑓:𝐵1-1-onto𝐷} ↔ 𝑦:𝐵1-1-onto𝐷)
3718cnvex 7948 . . . . . . . 8 ∈ V
3834, 20coex 7953 . . . . . . . 8 (𝑦𝑔) ∈ V
3937, 38coex 7953 . . . . . . 7 ( ∘ (𝑦𝑔)) ∈ V
40 f1oeq1 6837 . . . . . . 7 (𝑓 = ( ∘ (𝑦𝑔)) → (𝑓:𝐴1-1-onto𝐶 ↔ ( ∘ (𝑦𝑔)):𝐴1-1-onto𝐶))
4139, 40elab 3681 . . . . . 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 6287 . . . . . . . . . . 11 (((𝑥) ∘ 𝑔) ∘ 𝑔) = ((𝑥) ∘ (𝑔𝑔))
45 f1ococnv1 6878 . . . . . . . . . . . . . 14 (𝑔:𝐴1-1-onto𝐵 → (𝑔𝑔) = ( I ↾ 𝐴))
4645ad2antrr 726 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑔𝑔) = ( I ↾ 𝐴))
4746coeq2d 5876 . . . . . . . . . . . 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 6849 . . . . . . . . . . . . 13 ((𝑥):𝐴1-1-onto𝐷 → (𝑥):𝐴𝐷)
50 fcoi1 6783 . . . . . . . . . . . . 13 ((𝑥):𝐴𝐷 → ((𝑥) ∘ ( I ↾ 𝐴)) = (𝑥))
5148, 49, 503syl 18 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ ( I ↾ 𝐴)) = (𝑥))
5247, 51eqtrd 2775 . . . . . . . . . . 11 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) ∘ (𝑔𝑔)) = (𝑥))
5344, 52eqtr2id 2788 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (𝑥) = (((𝑥) ∘ 𝑔) ∘ 𝑔))
54 coass 6287 . . . . . . . . . . 11 (() ∘ (𝑦𝑔)) = ( ∘ ( ∘ (𝑦𝑔)))
55 f1ococnv2 6876 . . . . . . . . . . . . . 14 (:𝐶1-1-onto𝐷 → () = ( I ↾ 𝐷))
5655ad2antlr 727 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → () = ( I ↾ 𝐷))
5756coeq1d 5875 . . . . . . . . . . . 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 6849 . . . . . . . . . . . . 13 ((𝑦𝑔):𝐴1-1-onto𝐷 → (𝑦𝑔):𝐴𝐷)
60 fcoi2 6784 . . . . . . . . . . . . 13 ((𝑦𝑔):𝐴𝐷 → (( I ↾ 𝐷) ∘ (𝑦𝑔)) = (𝑦𝑔))
6158, 59, 603syl 18 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (( I ↾ 𝐷) ∘ (𝑦𝑔)) = (𝑦𝑔))
6257, 61eqtrd 2775 . . . . . . . . . . 11 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → (() ∘ (𝑦𝑔)) = (𝑦𝑔))
6354, 62eqtr3id 2789 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ( ∘ ( ∘ (𝑦𝑔))) = (𝑦𝑔))
6453, 63eqeq12d 2751 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ (((𝑥) ∘ 𝑔) ∘ 𝑔) = (𝑦𝑔)))
65 eqcom 2742 . . . . . . . . 9 ((((𝑥) ∘ 𝑔) ∘ 𝑔) = (𝑦𝑔) ↔ (𝑦𝑔) = (((𝑥) ∘ 𝑔) ∘ 𝑔))
6664, 65bitrdi 287 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ (𝑦𝑔) = (((𝑥) ∘ 𝑔) ∘ 𝑔)))
67 f1of1 6848 . . . . . . . . . 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 6849 . . . . . . . . . 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 6849 . . . . . . . . . 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 1370 . . . . . . . 8 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → ((𝑥) = ( ∘ ( ∘ (𝑦𝑔))) ↔ 𝑥 = ( ∘ (𝑦𝑔))))
76 f1ofo 6856 . . . . . . . . . 10 (𝑔:𝐴1-1-onto𝐵𝑔:𝐴onto𝐵)
7776ad2antrr 726 . . . . . . . . 9 (((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) ∧ (𝑥:𝐴1-1-onto𝐶𝑦:𝐵1-1-onto𝐷)) → 𝑔:𝐴onto𝐵)
78 f1ofn 6850 . . . . . . . . . 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 6850 . . . . . . . . . 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 1370 . . . . . . . 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 9028 . . . 4 ((𝑔:𝐴1-1-onto𝐵:𝐶1-1-onto𝐷) → {𝑓𝑓:𝐴1-1-onto𝐶} ≈ {𝑓𝑓:𝐵1-1-onto𝐷})
8988exlimivv 1930 . . 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 1537  wex 1776  wcel 2106  {cab 2712  Vcvv 3478   class class class wbr 5148   I cid 5582  ccnv 5688  cres 5691  ccom 5693   Fn wfn 6558  wf 6559  1-1wf1 6560  ontowfo 6561  1-1-ontowf1o 6562  cen 8981
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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8867  df-en 8985
This theorem is referenced by:  poimirlem9  37616
  Copyright terms: Public domain W3C validator