Theorem onfin2 9151

Description: A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.)

Assertion

Ref	Expression
onfin2	⊢ ω = (On ∩ Fin)

Proof of Theorem onfin2

Step	Hyp	Ref	Expression
1		nnon 7823	. . . . 5 ⊢ (𝑥 ∈ ω → 𝑥 ∈ On)
2		onfin 9149	. . . . . 6 ⊢ (𝑥 ∈ On → (𝑥 ∈ Fin ↔ 𝑥 ∈ ω))
3	2	biimprcd 250	. . . . 5 ⊢ (𝑥 ∈ ω → (𝑥 ∈ On → 𝑥 ∈ Fin))
4	1, 3	jcai 516	. . . 4 ⊢ (𝑥 ∈ ω → (𝑥 ∈ On ∧ 𝑥 ∈ Fin))
5	2	biimpa 476	. . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ Fin) → 𝑥 ∈ ω)
6	4, 5	impbii 209	. . 3 ⊢ (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ 𝑥 ∈ Fin))
7		elin 3905	. . 3 ⊢ (𝑥 ∈ (On ∩ Fin) ↔ (𝑥 ∈ On ∧ 𝑥 ∈ Fin))
8	6, 7	bitr4i 278	. 2 ⊢ (𝑥 ∈ ω ↔ 𝑥 ∈ (On ∩ Fin))
9	8	eqriv 2733	1 ⊢ ω = (On ∩ Fin)

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∩ cin 3888  Oncon0 6323  ωcom 7817  Fincfn 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-om 7818  df-1o 8405  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897

This theorem is referenced by:  cantnfcl  9588  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1b  10160  sdom2en01  10224  fin23lem26  10247  fin56  10315  fin1a2lem9  10330  fzfi  13934  fz1isolem  14423  ackbijnn  15793  hauspwdom  23466  fineqvomon  35262  0finon  43875  1finon  43876  2finon  43877  3finon  43878  4finon  43879  finona1cl  43880  finonex  43881  dfom6  43958