Metamath Proof Explorer

Theorem cardf2

Description: The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion cardf2 ${⊢}\mathrm{card}:\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}⟶\mathrm{On}$

Proof

Step Hyp Ref Expression
1 df-card ${⊢}\mathrm{card}=\left({x}\in \mathrm{V}⟼\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {x}\right\}\right)$
2 1 funmpt2 ${⊢}\mathrm{Fun}\mathrm{card}$
3 rabab ${⊢}\left\{{x}\in \mathrm{V}|\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {x}\right\}\in \mathrm{V}\right\}=\left\{{x}|\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {x}\right\}\in \mathrm{V}\right\}$
4 1 dmmpt ${⊢}\mathrm{dom}\mathrm{card}=\left\{{x}\in \mathrm{V}|\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {x}\right\}\in \mathrm{V}\right\}$
5 intexrab ${⊢}\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}↔\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {x}\right\}\in \mathrm{V}$
6 5 abbii ${⊢}\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}=\left\{{x}|\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {x}\right\}\in \mathrm{V}\right\}$
7 3 4 6 3eqtr4i ${⊢}\mathrm{dom}\mathrm{card}=\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}$
8 df-fn ${⊢}\mathrm{card}Fn\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}↔\left(\mathrm{Fun}\mathrm{card}\wedge \mathrm{dom}\mathrm{card}=\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}\right)$
9 2 7 8 mpbir2an ${⊢}\mathrm{card}Fn\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}$
10 simpr ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}$
11 vex ${⊢}{w}\in \mathrm{V}$
12 10 11 eqeltrrdi ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to \bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\in \mathrm{V}$
13 intex ${⊢}\left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\ne \varnothing ↔\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\in \mathrm{V}$
14 12 13 sylibr ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\ne \varnothing$
15 rabn0 ${⊢}\left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\ne \varnothing ↔\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {z}$
16 14 15 sylib ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to \exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {z}$
17 vex ${⊢}{z}\in \mathrm{V}$
18 breq2 ${⊢}{x}={z}\to \left({y}\approx {x}↔{y}\approx {z}\right)$
19 18 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}↔\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {z}\right)$
20 17 19 elab ${⊢}{z}\in \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}↔\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {z}$
21 16 20 sylibr ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to {z}\in \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}$
22 ssrab2 ${⊢}\left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\subseteq \mathrm{On}$
23 oninton ${⊢}\left(\left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\subseteq \mathrm{On}\wedge \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\ne \varnothing \right)\to \bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\in \mathrm{On}$
24 22 14 23 sylancr ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to \bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\in \mathrm{On}$
25 10 24 eqeltrd ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to {w}\in \mathrm{On}$
26 21 25 jca ${⊢}\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\to \left({z}\in \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}\wedge {w}\in \mathrm{On}\right)$
27 26 ssopab2i ${⊢}\left\{⟨{z},{w}⟩|\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\right\}\subseteq \left\{⟨{z},{w}⟩|\left({z}\in \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}\wedge {w}\in \mathrm{On}\right)\right\}$
28 df-card ${⊢}\mathrm{card}=\left({z}\in \mathrm{V}⟼\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)$
29 df-mpt ${⊢}\left({z}\in \mathrm{V}⟼\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)=\left\{⟨{z},{w}⟩|\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\right\}$
30 28 29 eqtri ${⊢}\mathrm{card}=\left\{⟨{z},{w}⟩|\left({z}\in \mathrm{V}\wedge {w}=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {z}\right\}\right)\right\}$
31 df-xp ${⊢}\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}×\mathrm{On}=\left\{⟨{z},{w}⟩|\left({z}\in \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}\wedge {w}\in \mathrm{On}\right)\right\}$
32 27 30 31 3sstr4i ${⊢}\mathrm{card}\subseteq \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}×\mathrm{On}$
33 dff2 ${⊢}\mathrm{card}:\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}⟶\mathrm{On}↔\left(\mathrm{card}Fn\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}\wedge \mathrm{card}\subseteq \left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}×\mathrm{On}\right)$
34 9 32 33 mpbir2an ${⊢}\mathrm{card}:\left\{{x}|\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{y}\approx {x}\right\}⟶\mathrm{On}$