This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hartogs

Description: The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 and hartogslem2 ) proof can be given using the axiom of choice, see ondomon . As its label indicates, this result is used to justify the definition of the Hartogs function df-har . (Contributed by Jeff Hankins, 22-Oct-2009) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion hartogs ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On )

Proof

Step Hyp Ref Expression
1 onelon ⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ∈ On )
2 vex ⊢ 𝑧 ∈ V
3 onelss ⊢ ( 𝑧 ∈ On → ( 𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧 ) )
4 3 imp ⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ⊆ 𝑧 )
5 ssdomg ⊢ ( 𝑧 ∈ V → ( 𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧 ) )
6 2 4 5 mpsyl ⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ≼ 𝑧 )
7 1 6 jca ⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝑧 ) )
8 domtr ⊢ ( ( 𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴 ) → 𝑦 ≼ 𝐴 )
9 8 anim2i ⊢ ( ( 𝑦 ∈ On ∧ ( 𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴 ) ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) )
10 9 anassrs ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝑧 ) ∧ 𝑧 ≼ 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) )
11 7 10 sylan ⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑧 ≼ 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) )
12 11 exp31 ⊢ ( 𝑧 ∈ On → ( 𝑦 ∈ 𝑧 → ( 𝑧 ≼ 𝐴 → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) ) )
13 12 com12 ⊢ ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ On → ( 𝑧 ≼ 𝐴 → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) ) )
14 13 impd ⊢ ( 𝑦 ∈ 𝑧 → ( ( 𝑧 ∈ On ∧ 𝑧 ≼ 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) )
15 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≼ 𝐴 ↔ 𝑧 ≼ 𝐴 ) )
16 15 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ↔ ( 𝑧 ∈ On ∧ 𝑧 ≼ 𝐴 ) )
17 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≼ 𝐴 ↔ 𝑦 ≼ 𝐴 ) )
18 17 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ↔ ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) )
19 14 16 18 3imtr4g ⊢ ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) )
20 19 imp ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } )
21 20 gen2 ⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } )
22 dftr2 ⊢ ( Tr { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) )
23 21 22 mpbir ⊢ Tr { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 }
24 ssrab2 ⊢ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ⊆ On
25 ordon ⊢ Ord On
26 trssord ⊢ ( ( Tr { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∧ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ⊆ On ∧ Ord On ) → Ord { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } )
27 23 24 25 26 mp3an ⊢ Ord { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 }
28 eqid ⊢ { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
29 eqid ⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑔 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑔 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) } = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑔 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑔 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) }
30 28 29 hartogslem2 ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ V )
31 elong ⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ V → ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On ↔ Ord { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) )
32 30 31 syl ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On ↔ Ord { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) )
33 27 32 mpbiri ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On )