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

Theorem mapen 9166
Description: Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
mapen ((𝐴𝐵𝐶𝐷) → (𝐴m 𝐶) ≈ (𝐵m 𝐷))

Proof of Theorem mapen
Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 8974 . 2 (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
2 bren 8974 . 2 (𝐶𝐷 ↔ ∃𝑔 𝑔:𝐶1-1-onto𝐷)
3 exdistrv 1952 . . 3 (∃𝑓𝑔(𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ↔ (∃𝑓 𝑓:𝐴1-1-onto𝐵 ∧ ∃𝑔 𝑔:𝐶1-1-onto𝐷))
4 ovexd 7455 . . . . 5 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝐴m 𝐶) ∈ V)
5 ovexd 7455 . . . . 5 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝐵m 𝐷) ∈ V)
6 elmapi 8868 . . . . . . 7 (𝑥 ∈ (𝐴m 𝐶) → 𝑥:𝐶𝐴)
7 f1of 6839 . . . . . . . . . . 11 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴𝐵)
87adantr 480 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑓:𝐴𝐵)
9 fco 6747 . . . . . . . . . 10 ((𝑓:𝐴𝐵𝑥:𝐶𝐴) → (𝑓𝑥):𝐶𝐵)
108, 9sylan 579 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ 𝑥:𝐶𝐴) → (𝑓𝑥):𝐶𝐵)
11 f1ocnv 6851 . . . . . . . . . . . 12 (𝑔:𝐶1-1-onto𝐷𝑔:𝐷1-1-onto𝐶)
1211adantl 481 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑔:𝐷1-1-onto𝐶)
13 f1of 6839 . . . . . . . . . . 11 (𝑔:𝐷1-1-onto𝐶𝑔:𝐷𝐶)
1412, 13syl 17 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑔:𝐷𝐶)
1514adantr 480 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ 𝑥:𝐶𝐴) → 𝑔:𝐷𝐶)
1610, 15fcod 6749 . . . . . . . 8 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ 𝑥:𝐶𝐴) → ((𝑓𝑥) ∘ 𝑔):𝐷𝐵)
1716ex 412 . . . . . . 7 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝑥:𝐶𝐴 → ((𝑓𝑥) ∘ 𝑔):𝐷𝐵))
186, 17syl5 34 . . . . . 6 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝑥 ∈ (𝐴m 𝐶) → ((𝑓𝑥) ∘ 𝑔):𝐷𝐵))
19 f1ofo 6846 . . . . . . . . . 10 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴onto𝐵)
2019adantr 480 . . . . . . . . 9 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑓:𝐴onto𝐵)
21 forn 6814 . . . . . . . . 9 (𝑓:𝐴onto𝐵 → ran 𝑓 = 𝐵)
2220, 21syl 17 . . . . . . . 8 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → ran 𝑓 = 𝐵)
23 vex 3475 . . . . . . . . 9 𝑓 ∈ V
2423rnex 7918 . . . . . . . 8 ran 𝑓 ∈ V
2522, 24eqeltrrdi 2838 . . . . . . 7 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝐵 ∈ V)
26 f1ofo 6846 . . . . . . . . . 10 (𝑔:𝐶1-1-onto𝐷𝑔:𝐶onto𝐷)
2726adantl 481 . . . . . . . . 9 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑔:𝐶onto𝐷)
28 forn 6814 . . . . . . . . 9 (𝑔:𝐶onto𝐷 → ran 𝑔 = 𝐷)
2927, 28syl 17 . . . . . . . 8 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → ran 𝑔 = 𝐷)
30 vex 3475 . . . . . . . . 9 𝑔 ∈ V
3130rnex 7918 . . . . . . . 8 ran 𝑔 ∈ V
3229, 31eqeltrrdi 2838 . . . . . . 7 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝐷 ∈ V)
3325, 32elmapd 8859 . . . . . 6 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (((𝑓𝑥) ∘ 𝑔) ∈ (𝐵m 𝐷) ↔ ((𝑓𝑥) ∘ 𝑔):𝐷𝐵))
3418, 33sylibrd 259 . . . . 5 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝑥 ∈ (𝐴m 𝐶) → ((𝑓𝑥) ∘ 𝑔) ∈ (𝐵m 𝐷)))
35 elmapi 8868 . . . . . . 7 (𝑦 ∈ (𝐵m 𝐷) → 𝑦:𝐷𝐵)
36 f1ocnv 6851 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto𝐵𝑓:𝐵1-1-onto𝐴)
3736adantr 480 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑓:𝐵1-1-onto𝐴)
38 f1of 6839 . . . . . . . . . . 11 (𝑓:𝐵1-1-onto𝐴𝑓:𝐵𝐴)
3937, 38syl 17 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑓:𝐵𝐴)
4039adantr 480 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ 𝑦:𝐷𝐵) → 𝑓:𝐵𝐴)
41 id 22 . . . . . . . . . 10 (𝑦:𝐷𝐵𝑦:𝐷𝐵)
42 f1of 6839 . . . . . . . . . . 11 (𝑔:𝐶1-1-onto𝐷𝑔:𝐶𝐷)
4342adantl 481 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝑔:𝐶𝐷)
44 fco 6747 . . . . . . . . . 10 ((𝑦:𝐷𝐵𝑔:𝐶𝐷) → (𝑦𝑔):𝐶𝐵)
4541, 43, 44syl2anr 596 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ 𝑦:𝐷𝐵) → (𝑦𝑔):𝐶𝐵)
4640, 45fcod 6749 . . . . . . . 8 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ 𝑦:𝐷𝐵) → (𝑓 ∘ (𝑦𝑔)):𝐶𝐴)
4746ex 412 . . . . . . 7 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝑦:𝐷𝐵 → (𝑓 ∘ (𝑦𝑔)):𝐶𝐴))
4835, 47syl5 34 . . . . . 6 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝑦 ∈ (𝐵m 𝐷) → (𝑓 ∘ (𝑦𝑔)):𝐶𝐴))
49 f1odm 6843 . . . . . . . . 9 (𝑓:𝐴1-1-onto𝐵 → dom 𝑓 = 𝐴)
5049adantr 480 . . . . . . . 8 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → dom 𝑓 = 𝐴)
5123dmex 7917 . . . . . . . 8 dom 𝑓 ∈ V
5250, 51eqeltrrdi 2838 . . . . . . 7 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝐴 ∈ V)
53 f1odm 6843 . . . . . . . . 9 (𝑔:𝐶1-1-onto𝐷 → dom 𝑔 = 𝐶)
5453adantl 481 . . . . . . . 8 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → dom 𝑔 = 𝐶)
5530dmex 7917 . . . . . . . 8 dom 𝑔 ∈ V
5654, 55eqeltrrdi 2838 . . . . . . 7 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → 𝐶 ∈ V)
5752, 56elmapd 8859 . . . . . 6 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → ((𝑓 ∘ (𝑦𝑔)) ∈ (𝐴m 𝐶) ↔ (𝑓 ∘ (𝑦𝑔)):𝐶𝐴))
5848, 57sylibrd 259 . . . . 5 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝑦 ∈ (𝐵m 𝐷) → (𝑓 ∘ (𝑦𝑔)) ∈ (𝐴m 𝐶)))
59 coass 6269 . . . . . . . . . . 11 ((𝑓𝑓) ∘ (𝑦𝑔)) = (𝑓 ∘ (𝑓 ∘ (𝑦𝑔)))
60 f1ococnv2 6866 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1-onto𝐵 → (𝑓𝑓) = ( I ↾ 𝐵))
6160ad2antrr 725 . . . . . . . . . . . . 13 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑓𝑓) = ( I ↾ 𝐵))
6261coeq1d 5864 . . . . . . . . . . . 12 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑓) ∘ (𝑦𝑔)) = (( I ↾ 𝐵) ∘ (𝑦𝑔)))
6345adantrl 715 . . . . . . . . . . . . 13 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑦𝑔):𝐶𝐵)
64 fcoi2 6772 . . . . . . . . . . . . 13 ((𝑦𝑔):𝐶𝐵 → (( I ↾ 𝐵) ∘ (𝑦𝑔)) = (𝑦𝑔))
6563, 64syl 17 . . . . . . . . . . . 12 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (( I ↾ 𝐵) ∘ (𝑦𝑔)) = (𝑦𝑔))
6662, 65eqtrd 2768 . . . . . . . . . . 11 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑓) ∘ (𝑦𝑔)) = (𝑦𝑔))
6759, 66eqtr3id 2782 . . . . . . . . . 10 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑓 ∘ (𝑓 ∘ (𝑦𝑔))) = (𝑦𝑔))
6867eqeq2d 2739 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) = (𝑓 ∘ (𝑓 ∘ (𝑦𝑔))) ↔ (𝑓𝑥) = (𝑦𝑔)))
69 coass 6269 . . . . . . . . . . . 12 (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔) = ((𝑓𝑥) ∘ (𝑔𝑔))
70 f1ococnv1 6868 . . . . . . . . . . . . . . 15 (𝑔:𝐶1-1-onto𝐷 → (𝑔𝑔) = ( I ↾ 𝐶))
7170ad2antlr 726 . . . . . . . . . . . . . 14 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑔𝑔) = ( I ↾ 𝐶))
7271coeq2d 5865 . . . . . . . . . . . . 13 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) ∘ (𝑔𝑔)) = ((𝑓𝑥) ∘ ( I ↾ 𝐶)))
7310adantrr 716 . . . . . . . . . . . . . 14 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑓𝑥):𝐶𝐵)
74 fcoi1 6771 . . . . . . . . . . . . . 14 ((𝑓𝑥):𝐶𝐵 → ((𝑓𝑥) ∘ ( I ↾ 𝐶)) = (𝑓𝑥))
7573, 74syl 17 . . . . . . . . . . . . 13 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) ∘ ( I ↾ 𝐶)) = (𝑓𝑥))
7672, 75eqtrd 2768 . . . . . . . . . . . 12 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) ∘ (𝑔𝑔)) = (𝑓𝑥))
7769, 76eqtrid 2780 . . . . . . . . . . 11 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔) = (𝑓𝑥))
7877eqeq2d 2739 . . . . . . . . . 10 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑦𝑔) = (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔) ↔ (𝑦𝑔) = (𝑓𝑥)))
79 eqcom 2735 . . . . . . . . . 10 ((𝑦𝑔) = (𝑓𝑥) ↔ (𝑓𝑥) = (𝑦𝑔))
8078, 79bitrdi 287 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑦𝑔) = (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔) ↔ (𝑓𝑥) = (𝑦𝑔)))
8168, 80bitr4d 282 . . . . . . . 8 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) = (𝑓 ∘ (𝑓 ∘ (𝑦𝑔))) ↔ (𝑦𝑔) = (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔)))
82 f1of1 6838 . . . . . . . . . 10 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴1-1𝐵)
8382ad2antrr 725 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → 𝑓:𝐴1-1𝐵)
84 simprl 770 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → 𝑥:𝐶𝐴)
8546adantrl 715 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑓 ∘ (𝑦𝑔)):𝐶𝐴)
86 cocan1 7300 . . . . . . . . 9 ((𝑓:𝐴1-1𝐵𝑥:𝐶𝐴 ∧ (𝑓 ∘ (𝑦𝑔)):𝐶𝐴) → ((𝑓𝑥) = (𝑓 ∘ (𝑓 ∘ (𝑦𝑔))) ↔ 𝑥 = (𝑓 ∘ (𝑦𝑔))))
8783, 84, 85, 86syl3anc 1369 . . . . . . . 8 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) = (𝑓 ∘ (𝑓 ∘ (𝑦𝑔))) ↔ 𝑥 = (𝑓 ∘ (𝑦𝑔))))
8827adantr 480 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → 𝑔:𝐶onto𝐷)
89 ffn 6722 . . . . . . . . . 10 (𝑦:𝐷𝐵𝑦 Fn 𝐷)
9089ad2antll 728 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → 𝑦 Fn 𝐷)
9116adantrr 716 . . . . . . . . . 10 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) ∘ 𝑔):𝐷𝐵)
9291ffnd 6723 . . . . . . . . 9 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑓𝑥) ∘ 𝑔) Fn 𝐷)
93 cocan2 7301 . . . . . . . . 9 ((𝑔:𝐶onto𝐷𝑦 Fn 𝐷 ∧ ((𝑓𝑥) ∘ 𝑔) Fn 𝐷) → ((𝑦𝑔) = (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑓𝑥) ∘ 𝑔)))
9488, 90, 92, 93syl3anc 1369 . . . . . . . 8 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → ((𝑦𝑔) = (((𝑓𝑥) ∘ 𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑓𝑥) ∘ 𝑔)))
9581, 87, 943bitr3d 309 . . . . . . 7 (((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) ∧ (𝑥:𝐶𝐴𝑦:𝐷𝐵)) → (𝑥 = (𝑓 ∘ (𝑦𝑔)) ↔ 𝑦 = ((𝑓𝑥) ∘ 𝑔)))
9695ex 412 . . . . . 6 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → ((𝑥:𝐶𝐴𝑦:𝐷𝐵) → (𝑥 = (𝑓 ∘ (𝑦𝑔)) ↔ 𝑦 = ((𝑓𝑥) ∘ 𝑔))))
976, 35, 96syl2ani 606 . . . . 5 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → ((𝑥 ∈ (𝐴m 𝐶) ∧ 𝑦 ∈ (𝐵m 𝐷)) → (𝑥 = (𝑓 ∘ (𝑦𝑔)) ↔ 𝑦 = ((𝑓𝑥) ∘ 𝑔))))
984, 5, 34, 58, 97en3d 9010 . . . 4 ((𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝐴m 𝐶) ≈ (𝐵m 𝐷))
9998exlimivv 1928 . . 3 (∃𝑓𝑔(𝑓:𝐴1-1-onto𝐵𝑔:𝐶1-1-onto𝐷) → (𝐴m 𝐶) ≈ (𝐵m 𝐷))
1003, 99sylbir 234 . 2 ((∃𝑓 𝑓:𝐴1-1-onto𝐵 ∧ ∃𝑔 𝑔:𝐶1-1-onto𝐷) → (𝐴m 𝐶) ≈ (𝐵m 𝐷))
1011, 2, 100syl2anb 597 1 ((𝐴𝐵𝐶𝐷) → (𝐴m 𝐶) ≈ (𝐵m 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1534  wex 1774  wcel 2099  Vcvv 3471   class class class wbr 5148   I cid 5575  ccnv 5677  dom cdm 5678  ran crn 5679  cres 5680  ccom 5682   Fn wfn 6543  wf 6544  1-1wf1 6545  ontowfo 6546  1-1-ontowf1o 6547  (class class class)co 7420  m cmap 8845  cen 8961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-map 8847  df-en 8965
This theorem is referenced by:  mapdom1  9167  mapdom2  9173  pwen  9175  mappwen  10136  mapdjuen  10204  cfpwsdom  10608  rpnnen  16204  rexpen  16205  enrelmap  43427
  Copyright terms: Public domain W3C validator