# Metamath Proof Explorer

## Theorem harval2

Description: An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harval2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left({A}\right)=\bigcap \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}$

### Proof

Step Hyp Ref Expression
1 harval ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left({A}\right)=\left\{{y}\in \mathrm{On}|{y}\preccurlyeq {A}\right\}$
2 1 adantr ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\right)\to \mathrm{har}\left({A}\right)=\left\{{y}\in \mathrm{On}|{y}\preccurlyeq {A}\right\}$
3 sdomel ${⊢}\left({y}\in \mathrm{On}\wedge {x}\in \mathrm{On}\right)\to \left({y}\prec {x}\to {y}\in {x}\right)$
4 domsdomtr ${⊢}\left({y}\preccurlyeq {A}\wedge {A}\prec {x}\right)\to {y}\prec {x}$
5 3 4 impel ${⊢}\left(\left({y}\in \mathrm{On}\wedge {x}\in \mathrm{On}\right)\wedge \left({y}\preccurlyeq {A}\wedge {A}\prec {x}\right)\right)\to {y}\in {x}$
6 5 an4s ${⊢}\left(\left({y}\in \mathrm{On}\wedge {y}\preccurlyeq {A}\right)\wedge \left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\right)\to {y}\in {x}$
7 6 ancoms ${⊢}\left(\left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\wedge \left({y}\in \mathrm{On}\wedge {y}\preccurlyeq {A}\right)\right)\to {y}\in {x}$
8 7 3impb ${⊢}\left(\left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\wedge {y}\in \mathrm{On}\wedge {y}\preccurlyeq {A}\right)\to {y}\in {x}$
9 8 rabssdv ${⊢}\left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\to \left\{{y}\in \mathrm{On}|{y}\preccurlyeq {A}\right\}\subseteq {x}$
10 9 adantl ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\right)\to \left\{{y}\in \mathrm{On}|{y}\preccurlyeq {A}\right\}\subseteq {x}$
11 2 10 eqsstrd ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \left({x}\in \mathrm{On}\wedge {A}\prec {x}\right)\right)\to \mathrm{har}\left({A}\right)\subseteq {x}$
12 11 expr ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {x}\in \mathrm{On}\right)\to \left({A}\prec {x}\to \mathrm{har}\left({A}\right)\subseteq {x}\right)$
13 12 ralrimiva ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({A}\prec {x}\to \mathrm{har}\left({A}\right)\subseteq {x}\right)$
14 ssintrab ${⊢}\mathrm{har}\left({A}\right)\subseteq \bigcap \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}↔\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({A}\prec {x}\to \mathrm{har}\left({A}\right)\subseteq {x}\right)$
15 13 14 sylibr ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left({A}\right)\subseteq \bigcap \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}$
16 breq2 ${⊢}{x}=\mathrm{har}\left({A}\right)\to \left({A}\prec {x}↔{A}\prec \mathrm{har}\left({A}\right)\right)$
17 harcl ${⊢}\mathrm{har}\left({A}\right)\in \mathrm{On}$
18 17 a1i ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left({A}\right)\in \mathrm{On}$
19 harsdom ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to {A}\prec \mathrm{har}\left({A}\right)$
20 16 18 19 elrabd ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left({A}\right)\in \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}$
21 intss1 ${⊢}\mathrm{har}\left({A}\right)\in \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}\to \bigcap \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}\subseteq \mathrm{har}\left({A}\right)$
22 20 21 syl ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \bigcap \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}\subseteq \mathrm{har}\left({A}\right)$
23 15 22 eqssd ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left({A}\right)=\bigcap \left\{{x}\in \mathrm{On}|{A}\prec {x}\right\}$