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 39147
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 ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
fsovd.a (𝜑𝐴𝑉)
fsovd.b (𝜑𝐵𝑊)
fsovfvd.g 𝐺 = (𝐴𝑂𝐵)
fsovcnvlem.h 𝐻 = (𝐵𝑂𝐴)
Assertion
Ref Expression
fsovcnvlem (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
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 3912 . . . . . . . . 9 {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴
32a1i 11 . . . . . . . 8 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ⊆ 𝐴)
41, 3sselpwd 5032 . . . . . . 7 (𝜑 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
54adantr 474 . . . . . 6 ((𝜑𝑦𝐵) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} ∈ 𝒫 𝐴)
65fmpttd 6634 . . . . 5 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴)
71pwexd 5079 . . . . . 6 (𝜑 → 𝒫 𝐴 ∈ V)
8 fsovd.b . . . . . 6 (𝜑𝐵𝑊)
97, 8elmapd 8136 . . . . 5 (𝜑 → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵) ↔ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}):𝐵⟶𝒫 𝐴))
106, 9mpbird 249 . . . 4 (𝜑 → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵))
1110adantr 474 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) ∈ (𝒫 𝐴𝑚 𝐵))
12 fsovfvd.g . . . 4 𝐺 = (𝐴𝑂𝐵)
13 fsovd.fs . . . . 5 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})))
1413, 1, 8fsovd 39142 . . . 4 (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
1512, 14syl5eq 2873 . . 3 (𝜑𝐺 = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})))
16 fsovcnvlem.h . . . 4 𝐻 = (𝐵𝑂𝐴)
17 oveq2 6913 . . . . . . . 8 (𝑎 = 𝑑 → (𝒫 𝑏𝑚 𝑎) = (𝒫 𝑏𝑚 𝑑))
18 rabeq 3405 . . . . . . . . 9 (𝑎 = 𝑑 → {𝑥𝑎𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑓𝑥)})
1918mpteq2dv 4968 . . . . . . . 8 (𝑎 = 𝑑 → (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2017, 19mpteq12dv 4956 . . . . . . 7 (𝑎 = 𝑑 → (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑏𝑚 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
21 pweq 4381 . . . . . . . . 9 (𝑏 = 𝑐 → 𝒫 𝑏 = 𝒫 𝑐)
2221oveq1d 6920 . . . . . . . 8 (𝑏 = 𝑐 → (𝒫 𝑏𝑚 𝑑) = (𝒫 𝑐𝑚 𝑑))
23 mpteq1 4960 . . . . . . . 8 (𝑏 = 𝑐 → (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))
2422, 23mpteq12dv 4956 . . . . . . 7 (𝑏 = 𝑐 → (𝑓 ∈ (𝒫 𝑏𝑚 𝑑) ↦ (𝑦𝑏 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
2520, 24cbvmpt2v 6995 . . . . . 6 (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝑎) ↦ (𝑦𝑏 ↦ {𝑥𝑎𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})))
26 eqid 2825 . . . . . . 7 V = V
27 fveq1 6432 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2827eleq2d 2892 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑦 ∈ (𝑔𝑥)))
2928rabbidv 3402 . . . . . . . . . 10 (𝑓 = 𝑔 → {𝑥𝑑𝑦 ∈ (𝑓𝑥)} = {𝑥𝑑𝑦 ∈ (𝑔𝑥)})
3029mpteq2dv 4968 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}) = (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
3130cbvmptv 4973 . . . . . . . 8 (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}))
32 eleq1w 2889 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑥)))
3332rabbidv 3402 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑥𝑑𝑦 ∈ (𝑔𝑥)} = {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
3433cbvmptv 4973 . . . . . . . . . 10 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)})
35 fveq2 6433 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑔𝑥) = (𝑔𝑣))
3635eleq2d 2892 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑢 ∈ (𝑔𝑥) ↔ 𝑢 ∈ (𝑔𝑣)))
3736cbvrabv 3412 . . . . . . . . . . 11 {𝑥𝑑𝑢 ∈ (𝑔𝑥)} = {𝑣𝑑𝑢 ∈ (𝑔𝑣)}
3837mpteq2i 4964 . . . . . . . . . 10 (𝑢𝑐 ↦ {𝑥𝑑𝑢 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
3934, 38eqtri 2849 . . . . . . . . 9 (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)}) = (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})
4039mpteq2i 4964 . . . . . . . 8 (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑔𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4131, 40eqtri 2849 . . . . . . 7 (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)})) = (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)}))
4226, 26, 41mpt2eq123i 6978 . . . . . 6 (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑓 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑦𝑐 ↦ {𝑥𝑑𝑦 ∈ (𝑓𝑥)}))) = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4313, 25, 423eqtri 2853 . . . . 5 𝑂 = (𝑑 ∈ V, 𝑐 ∈ V ↦ (𝑔 ∈ (𝒫 𝑐𝑚 𝑑) ↦ (𝑢𝑐 ↦ {𝑣𝑑𝑢 ∈ (𝑔𝑣)})))
4443, 8, 1fsovd 39142 . . . 4 (𝜑 → (𝐵𝑂𝐴) = (𝑔 ∈ (𝒫 𝐴𝑚 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
4516, 44syl5eq 2873 . . 3 (𝜑𝐻 = (𝑔 ∈ (𝒫 𝐴𝑚 𝐵) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)})))
46 fveq1 6432 . . . . . 6 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑔𝑣) = ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣))
4746eleq2d 2892 . . . . 5 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢 ∈ (𝑔𝑣) ↔ 𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)))
4847rabbidv 3402 . . . 4 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → {𝑣𝐵𝑢 ∈ (𝑔𝑣)} = {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})
4948mpteq2dv 4968 . . 3 (𝑔 = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ (𝑔𝑣)}) = (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}))
5011, 15, 45, 49fmptco 6646 . 2 (𝜑 → (𝐻𝐺) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})))
51 eqidd 2826 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}) = (𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)}))
52 eleq1w 2889 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (𝑦 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑥)))
5352rabbidv 3402 . . . . . . . . . . . 12 (𝑦 = 𝑣 → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
5453adantl 475 . . . . . . . . . . 11 ((((𝜑𝑢𝐴) ∧ 𝑣𝐵) ∧ 𝑦 = 𝑣) → {𝑥𝐴𝑦 ∈ (𝑓𝑥)} = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
55 simpr 479 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → 𝑣𝐵)
56 rabexg 5036 . . . . . . . . . . . . 13 (𝐴𝑉 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
571, 56syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
5857ad2antrr 719 . . . . . . . . . . 11 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ∈ V)
5951, 54, 55, 58fvmptd 6535 . . . . . . . . . 10 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) = {𝑥𝐴𝑣 ∈ (𝑓𝑥)})
6059eleq2d 2892 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)}))
61 fveq2 6433 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑓𝑥) = (𝑓𝑢))
6261eleq2d 2892 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑣 ∈ (𝑓𝑥) ↔ 𝑣 ∈ (𝑓𝑢)))
6362elrab3 3587 . . . . . . . . . 10 (𝑢𝐴 → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6463ad2antlr 720 . . . . . . . . 9 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ {𝑥𝐴𝑣 ∈ (𝑓𝑥)} ↔ 𝑣 ∈ (𝑓𝑢)))
6560, 64bitrd 271 . . . . . . . 8 (((𝜑𝑢𝐴) ∧ 𝑣𝐵) → (𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣) ↔ 𝑣 ∈ (𝑓𝑢)))
6665rabbidva 3401 . . . . . . 7 ((𝜑𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
6766adantlr 708 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
68 dfin5 3806 . . . . . . 7 (𝐵 ∩ (𝑓𝑢)) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)}
69 elmapi 8144 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
7069ad2antlr 720 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → 𝑓:𝐴⟶𝒫 𝐵)
71 simpr 479 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → 𝑢𝐴)
7270, 71ffvelrnd 6609 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ∈ 𝒫 𝐵)
7372elpwid 4390 . . . . . . . 8 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) ⊆ 𝐵)
74 sseqin2 4044 . . . . . . . 8 ((𝑓𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7573, 74sylib 210 . . . . . . 7 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝐵 ∩ (𝑓𝑢)) = (𝑓𝑢))
7668, 75syl5reqr 2876 . . . . . 6 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → (𝑓𝑢) = {𝑣𝐵𝑣 ∈ (𝑓𝑢)})
7767, 76eqtr4d 2864 . . . . 5 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) ∧ 𝑢𝐴) → {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)} = (𝑓𝑢))
7877mpteq2dva 4967 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = (𝑢𝐴 ↦ (𝑓𝑢)))
7969feqmptd 6496 . . . . 5 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8079adantl 475 . . . 4 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → 𝑓 = (𝑢𝐴 ↦ (𝑓𝑢)))
8178, 80eqtr4d 2864 . . 3 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝐴)) → (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)}) = 𝑓)
8281mpteq2dva 4967 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ (𝑢𝐴 ↦ {𝑣𝐵𝑢 ∈ ((𝑦𝐵 ↦ {𝑥𝐴𝑦 ∈ (𝑓𝑥)})‘𝑣)})) = (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓))
83 mptresid 5699 . . 3 (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵𝑚 𝐴))
8483a1i 11 . 2 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝐴) ↦ 𝑓) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
8550, 82, 843eqtrd 2865 1 (𝜑 → (𝐻𝐺) = ( I ↾ (𝒫 𝐵𝑚 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  {crab 3121  Vcvv 3414  cin 3797  wss 3798  𝒫 cpw 4378  cmpt 4952   I cid 5249  cres 5344  ccom 5346  wf 6119  cfv 6123  (class class class)co 6905  cmpt2 6907  𝑚 cmap 8122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-1st 7428  df-2nd 7429  df-map 8124
This theorem is referenced by:  fsovcnvd  39148
  Copyright terms: Public domain W3C validator