Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fsovcnvlem Structured version   Visualization version   GIF version

Theorem fsovcnvlem 41583
Description: The 𝑂 operator, which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021.)
Hypotheses
Ref Expression
fsovd.fs 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
fsovd.a (𝜑𝐴𝑉)
fsovd.b (𝜑𝐵𝑊)
fsovfvd.g 𝐺 = (𝐴𝑂𝐵)
fsovcnvlem.h 𝐻 = (𝐵𝑂𝐴)
Assertion
Ref Expression
fsovcnvlem (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵m 𝐴)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑥,𝑦   𝐵,𝑎,𝑏,𝑓,𝑦   𝜑,𝑎,𝑏,𝑓,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐺(𝑥,𝑦,𝑓,𝑎,𝑏)   𝐻(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑂(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑊(𝑥,𝑦,𝑓,𝑎,𝑏)

Proof of Theorem fsovcnvlem
Dummy variables 𝑐 𝑑 𝑔 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsovd.a . . . . . . . 8 (𝜑𝐴𝑉)
2 ssrab2 4018 . . . . . . . . 9 {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴
32a1i 11 . . . . . . . 8 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴)
41, 3sselpwd 5254 . . . . . . 7 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
54adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
65fmpttd 6984 . . . . 5 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴)
71pwexd 5306 . . . . . 6 (𝜑 → 𝒫 𝐴 ∈ V)
8 fsovd.b . . . . . 6 (𝜑𝐵𝑊)
97, 8elmapd 8604 . . . . 5 (𝜑 → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴m 𝐵) ↔ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴))
106, 9mpbird 256 . . . 4 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴m 𝐵))
1110adantr 481 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴m 𝐵))
12 fsovfvd.g . . . 4 𝐺 = (𝐴𝑂𝐵)
13 fsovd.fs . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
1413, 1, 8fsovd 41578 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
1512, 14eqtrid 2792 . . 3 (𝜑𝐺 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
16 fsovcnvlem.h . . . 4 𝐻 = (𝐵𝑂𝐴)
17 oveq2 7277 . . . . . . . 8 (𝑎 = 𝑑 → (𝒫 𝑏m 𝑎) = (𝒫 𝑏m 𝑑))
18 rabeq 3417 . . . . . . . . 9 (𝑎 = 𝑑 → {𝑥𝑎𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑓𝑥)})
1918mpteq2dv 5181 . . . . . . . 8 (𝑎 = 𝑑 → (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2017, 19mpteq12dv 5170 . . . . . . 7 (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑏m 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
21 pweq 4555 . . . . . . . . 9 (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
2221oveq1d 7284 . . . . . . . 8 (𝑏 = 𝑐 → (𝒫 𝑏m 𝑑) = (𝒫 𝑐m 𝑑))
23 mpteq1 5172 . . . . . . . 8 (𝑏 = 𝑐 → (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2422, 23mpteq12dv 5170 . . . . . . 7 (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏m 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
2520, 24cbvmpov 7362 . . . . . 6 (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
26 eqid 2740 . . . . . . 7 V = V
27 fveq1 6768 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2827eleq2d 2826 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑦 ∈ (𝑔𝑥)))
2928rabbidv 3413 . . . . . . . . . 10 (𝑓 = 𝑔 → {𝑥𝑑𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑔𝑥)})
3029mpteq2dv 5181 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
3130cbvmptv 5192 . . . . . . . 8 (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
32 eleq1w 2823 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑥)))
3332rabbidv 3413 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑥𝑑𝑦 ∈ (𝑔𝑥)} = {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
3433cbvmptv 5192 . . . . . . . . . 10 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
35 fveq2 6769 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑔𝑥) = (𝑔𝑣))
3635eleq2d 2826 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑢 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑣)))
3736cbvrabv 3425 . . . . . . . . . . 11 {𝑥𝑑𝑢 ∈ (𝑔𝑥)} = {𝑣𝑑𝑢 ∈ (𝑔𝑣)}
3837mpteq2i 5184 . . . . . . . . . 10 (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
3934, 38eqtri 2768 . . . . . . . . 9 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4039mpteq2i 5184 . . . . . . . 8 (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)})) = (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4131, 40eqtri 2768 . . . . . . 7 (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4226, 26, 41mpoeq123i 7343 . . . . . 6 (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4313, 25, 423eqtri 2772 . . . . 5 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4443, 8, 1fsovd 41578 . . . 4 (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴m 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
4516, 44eqtrid 2792 . . 3 (𝜑𝐻 = (𝑔 ∈ (𝒫 𝐴m 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
46 fveq1 6768 . . . . . 6 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑔𝑣) = ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣))
4746eleq2d 2826 . . . . 5 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢 ∈ (𝑔𝑣) ↔ 𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)))
4847rabbidv 3413 . . . 4 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → {𝑣𝐵𝑢 ∈ (𝑔𝑣)} = {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})
4948mpteq2dv 5181 . . 3 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)}) = (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}))
5011, 15, 45, 49fmptco 6996 . 2 (𝜑 → (𝐻𝐺) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})))
51 eqidd 2741 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}))
52 eleq1w 2823 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑥)))
5352rabbidv 3413 . . . . . . . . . . . 12 (𝑦 = 𝑣 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
5453adantl 482 . . . . . . . . . . 11 ((((𝜑𝑢𝐴) ∧ 𝑣𝐵) ∧ 𝑦 = 𝑣) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
55 simpr 485 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → 𝑣𝐵)
56 rabexg 5259 . . . . . . . . . . . . 13 (𝐴𝑉 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
571, 56syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
5857ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
5951, 54, 55, 58fvmptd 6877 . . . . . . . . . 10 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
6059eleq2d 2826 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)}))
61 fveq2 6769 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑓𝑥) = (𝑓𝑢))
6261eleq2d 2826 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑣 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
6362elrab3 3627 . . . . . . . . . 10 (𝑢𝐴 → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6463ad2antlr 724 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6560, 64bitrd 278 . . . . . . . 8 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓𝑢)))
6665rabbidva 3411 . . . . . . 7 ((𝜑𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
6766adantlr 712 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
68 elmapi 8612 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
6968ad2antlr 724 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
70 simpr 485 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → 𝑢𝐴)
7169, 70ffvelrnd 6957 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
7271elpwid 4550 . . . . . . . 8 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
73 sseqin2 4155 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7472, 73sylib 217 . . . . . . 7 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
75 dfin5 3900 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)}
7674, 75eqtr3di 2795 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
7767, 76eqtr4d 2783 . . . . 5 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = (𝑓𝑢))
7877mpteq2dva 5179 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = (𝑢𝐴 ↦ (𝑓𝑢)))
7968feqmptd 6832 . . . . 5 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8079adantl 482 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8178, 80eqtr4d 2783 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = 𝑓)
8281mpteq2dva 5179 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓))
83 mptresid 5956 . . . 4 ( I ↾ (𝒫 𝐵m 𝐴)) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓)
8483eqcomi 2749 . . 3 (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵m 𝐴))
8584a1i 11 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵m 𝐴)))
8650, 82, 853eqtrd 2784 1 (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵m 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1542  wcel 2110  {crab 3070  Vcvv 3431  cin 3891  wss 3892  𝒫 cpw 4539  cmpt 5162   I cid 5488  cres 5591  ccom 5593  wf 6427  cfv 6431  (class class class)co 7269  cmpo 7271  m cmap 8590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-ov 7272  df-oprab 7273  df-mpo 7274  df-1st 7818  df-2nd 7819  df-map 8592
This theorem is referenced by:  fsovcnvd  41584
  Copyright terms: Public domain W3C validator