Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hfuni Structured version   Visualization version   GIF version

Theorem hfuni 34254
Description: The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
Assertion
Ref Expression
hfuni (𝐴 ∈ Hf → 𝐴 ∈ Hf )

Proof of Theorem hfuni
StepHypRef Expression
1 rankuni 9506 . . 3 (rank‘ 𝐴) = (rank‘𝐴)
2 rankon 9438 . . . . . 6 (rank‘𝐴) ∈ On
32ontrci 6339 . . . . 5 Tr (rank‘𝐴)
4 df-tr 5178 . . . . 5 (Tr (rank‘𝐴) ↔ (rank‘𝐴) ⊆ (rank‘𝐴))
53, 4mpbi 233 . . . 4 (rank‘𝐴) ⊆ (rank‘𝐴)
6 elhf2g 34246 . . . . 5 (𝐴 ∈ Hf → (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω))
76ibi 270 . . . 4 (𝐴 ∈ Hf → (rank‘𝐴) ∈ ω)
8 rankon 9438 . . . . . . 7 (rank‘ 𝐴) ∈ On
91, 8eqeltrri 2837 . . . . . 6 (rank‘𝐴) ∈ On
109onordi 6338 . . . . 5 Ord (rank‘𝐴)
11 ordom 7675 . . . . 5 Ord ω
12 ordtr2 6277 . . . . 5 ((Ord (rank‘𝐴) ∧ Ord ω) → (( (rank‘𝐴) ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ∈ ω) → (rank‘𝐴) ∈ ω))
1310, 11, 12mp2an 692 . . . 4 (( (rank‘𝐴) ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ∈ ω) → (rank‘𝐴) ∈ ω)
145, 7, 13sylancr 590 . . 3 (𝐴 ∈ Hf → (rank‘𝐴) ∈ ω)
151, 14eqeltrid 2844 . 2 (𝐴 ∈ Hf → (rank‘ 𝐴) ∈ ω)
16 uniexg 7549 . . 3 (𝐴 ∈ Hf → 𝐴 ∈ V)
17 elhf2g 34246 . . 3 ( 𝐴 ∈ V → ( 𝐴 ∈ Hf ↔ (rank‘ 𝐴) ∈ ω))
1816, 17syl 17 . 2 (𝐴 ∈ Hf → ( 𝐴 ∈ Hf ↔ (rank‘ 𝐴) ∈ ω))
1915, 18mpbird 260 1 (𝐴 ∈ Hf → 𝐴 ∈ Hf )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wcel 2112  Vcvv 3422  wss 3882   cuni 4835  Tr wtr 5177  Ord word 6232  Oncon0 6233  cfv 6400  ωcom 7665  rankcrnk 9406   Hf chf 34242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-reg 9235  ax-inf2 9283
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-int 4876  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-om 7666  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-r1 9407  df-rank 9408  df-hf 34243
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator