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

Theorem fsovcnvlem 40357
 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 4055 . . . . . . . . 9 {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴
32a1i 11 . . . . . . . 8 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴)
41, 3sselpwd 5229 . . . . . . 7 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
54adantr 483 . . . . . 6 ((𝜑𝑦𝐵) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
65fmpttd 6878 . . . . 5 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴)
71pwexd 5279 . . . . . 6 (𝜑 → 𝒫 𝐴 ∈ V)
8 fsovd.b . . . . . 6 (𝜑𝐵𝑊)
97, 8elmapd 8419 . . . . 5 (𝜑 → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴m 𝐵) ↔ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴))
106, 9mpbird 259 . . . 4 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴m 𝐵))
1110adantr 483 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴m 𝐵))
12 fsovfvd.g . . . 4 𝐺 = (𝐴𝑂𝐵)
13 fsovd.fs . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
1413, 1, 8fsovd 40352 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
1512, 14syl5eq 2868 . . 3 (𝜑𝐺 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
16 fsovcnvlem.h . . . 4 𝐻 = (𝐵𝑂𝐴)
17 oveq2 7163 . . . . . . . 8 (𝑎 = 𝑑 → (𝒫 𝑏m 𝑎) = (𝒫 𝑏m 𝑑))
18 rabeq 3483 . . . . . . . . 9 (𝑎 = 𝑑 → {𝑥𝑎𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑓𝑥)})
1918mpteq2dv 5161 . . . . . . . 8 (𝑎 = 𝑑 → (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2017, 19mpteq12dv 5150 . . . . . . 7 (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑏m 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
21 pweq 4554 . . . . . . . . 9 (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
2221oveq1d 7170 . . . . . . . 8 (𝑏 = 𝑐 → (𝒫 𝑏m 𝑑) = (𝒫 𝑐m 𝑑))
23 mpteq1 5153 . . . . . . . 8 (𝑏 = 𝑐 → (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2422, 23mpteq12dv 5150 . . . . . . 7 (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏m 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
2520, 24cbvmpov 7248 . . . . . 6 (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
26 eqid 2821 . . . . . . 7 V = V
27 fveq1 6668 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2827eleq2d 2898 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑦 ∈ (𝑔𝑥)))
2928rabbidv 3480 . . . . . . . . . 10 (𝑓 = 𝑔 → {𝑥𝑑𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑔𝑥)})
3029mpteq2dv 5161 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
3130cbvmptv 5168 . . . . . . . 8 (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
32 eleq1w 2895 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑥)))
3332rabbidv 3480 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑥𝑑𝑦 ∈ (𝑔𝑥)} = {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
3433cbvmptv 5168 . . . . . . . . . 10 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
35 fveq2 6669 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑔𝑥) = (𝑔𝑣))
3635eleq2d 2898 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑢 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑣)))
3736cbvrabv 3491 . . . . . . . . . . 11 {𝑥𝑑𝑢 ∈ (𝑔𝑥)} = {𝑣𝑑𝑢 ∈ (𝑔𝑣)}
3837mpteq2i 5157 . . . . . . . . . 10 (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
3934, 38eqtri 2844 . . . . . . . . 9 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4039mpteq2i 5157 . . . . . . . 8 (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)})) = (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4131, 40eqtri 2844 . . . . . . 7 (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4226, 26, 41mpoeq123i 7229 . . . . . 6 (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4313, 25, 423eqtri 2848 . . . . 5 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐m 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4443, 8, 1fsovd 40352 . . . 4 (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴m 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
4516, 44syl5eq 2868 . . 3 (𝜑𝐻 = (𝑔 ∈ (𝒫 𝐴m 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
46 fveq1 6668 . . . . . 6 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑔𝑣) = ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣))
4746eleq2d 2898 . . . . 5 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢 ∈ (𝑔𝑣) ↔ 𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)))
4847rabbidv 3480 . . . 4 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → {𝑣𝐵𝑢 ∈ (𝑔𝑣)} = {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})
4948mpteq2dv 5161 . . 3 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)}) = (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}))
5011, 15, 45, 49fmptco 6890 . 2 (𝜑 → (𝐻𝐺) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})))
51 eqidd 2822 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}))
52 eleq1w 2895 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑥)))
5352rabbidv 3480 . . . . . . . . . . . 12 (𝑦 = 𝑣 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
5453adantl 484 . . . . . . . . . . 11 ((((𝜑𝑢𝐴) ∧ 𝑣𝐵) ∧ 𝑦 = 𝑣) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
55 simpr 487 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → 𝑣𝐵)
56 rabexg 5233 . . . . . . . . . . . . 13 (𝐴𝑉 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
571, 56syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
5857ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
5951, 54, 55, 58fvmptd 6774 . . . . . . . . . 10 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
6059eleq2d 2898 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)}))
61 fveq2 6669 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑓𝑥) = (𝑓𝑢))
6261eleq2d 2898 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑣 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
6362elrab3 3680 . . . . . . . . . 10 (𝑢𝐴 → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6463ad2antlr 725 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6560, 64bitrd 281 . . . . . . . 8 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓𝑢)))
6665rabbidva 3478 . . . . . . 7 ((𝜑𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
6766adantlr 713 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
68 dfin5 3943 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)}
69 elmapi 8427 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
7069ad2antlr 725 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
71 simpr 487 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → 𝑢𝐴)
7270, 71ffvelrnd 6851 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
7372elpwid 4549 . . . . . . . 8 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
74 sseqin2 4191 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7573, 74sylib 220 . . . . . . 7 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7668, 75syl5reqr 2871 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
7767, 76eqtr4d 2859 . . . . 5 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = (𝑓𝑢))
7877mpteq2dva 5160 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = (𝑢𝐴 ↦ (𝑓𝑢)))
7969feqmptd 6732 . . . . 5 (𝑓 ∈ (𝒫 𝐵m 𝐴) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8079adantl 484 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8178, 80eqtr4d 2859 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = 𝑓)
8281mpteq2dva 5160 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓))
83 mptresid 5917 . . . 4 ( I ↾ (𝒫 𝐵m 𝐴)) = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓)
8483eqcomi 2830 . . 3 (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵m 𝐴))
8584a1i 11 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵m 𝐴)))
8650, 82, 853eqtrd 2860 1 (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵m 𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {crab 3142  Vcvv 3494   ∩ cin 3934   ⊆ wss 3935  𝒫 cpw 4538   ↦ cmpt 5145   I cid 5458   ↾ cres 5556   ∘ ccom 5558  ⟶wf 6350  ‘cfv 6354  (class class class)co 7155   ∈ cmpo 7157   ↑m cmap 8405 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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-ov 7158  df-oprab 7159  df-mpo 7160  df-1st 7688  df-2nd 7689  df-map 8407 This theorem is referenced by:  fsovcnvd  40358
 Copyright terms: Public domain W3C validator