Theorem hartogs 9450

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem hartogs

Dummy variables 𝑔 𝑟 𝑠 𝑡 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onelon 6340	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On)
2		vex 3434	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
3		onelss 6357	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧))
4	3	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧)
5		ssdomg 8938	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧))
6	2, 4, 5	mpsyl 68	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ≼ 𝑧)
7	1, 6	jca 511	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝑧))
8		domtr 8945	. . . . . . . . . . . . 13 ⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴) → 𝑦 ≼ 𝐴)
9	8	anim2i 618	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ (𝑦 ≼ 𝑧 ∧ 𝑧 ≼ 𝐴)) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))
10	9	anassrs 467	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ On ∧ 𝑦 ≼ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))
11	7, 10	sylan 581	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))
12	11	exp31 419	. . . . . . . . 9 ⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → (𝑧 ≼ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))))
13	12	com12 32	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ On → (𝑧 ≼ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))))
14	13	impd 410	. . . . . . 7 ⊢ (𝑦 ∈ 𝑧 → ((𝑧 ∈ On ∧ 𝑧 ≼ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)))
15		breq1 5089	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ≼ 𝐴 ↔ 𝑧 ≼ 𝐴))
16	15	elrab 3635	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑧 ∈ On ∧ 𝑧 ≼ 𝐴))
17		breq1 5089	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ≼ 𝐴 ↔ 𝑦 ≼ 𝐴))
18	17	elrab 3635	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))
19	14, 16, 18	3imtr4g 296	. . . . . 6 ⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
20	19	imp 406	. . . . 5 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})
21	20	gen2 1798	. . . 4 ⊢ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})
22		dftr2 5195	. . . 4 ⊢ (Tr {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
23	21, 22	mpbir 231	. . 3 ⊢ Tr {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}
24		ssrab2 4021	. . 3 ⊢ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On
25		ordon 7722	. . 3 ⊢ Ord On
26		trssord 6332	. . 3 ⊢ ((Tr {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})
27	23, 24, 25, 26	mp3an 1464	. 2 ⊢ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}
28		eqid 2737	. . . 4 ⊢ {⟨𝑟, 𝑦⟩ ∣ (((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 2737	. . . 4 ⊢ {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑔‘𝑤) ∧ 𝑡 = (𝑔‘𝑧)) ∧ 𝑤 E 𝑧)} = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑔‘𝑤) ∧ 𝑡 = (𝑔‘𝑧)) ∧ 𝑤 E 𝑧)}
30	28, 29	hartogslem2 9449	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V)
31		elong 6323	. . 3 ⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
32	30, 31	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
33	27, 32	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1540   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  {crab 3390  Vcvv 3430   ∖ cdif 3887   ⊆ wss 3890   class class class wbr 5086  {copab 5148  Tr wtr 5193   I cid 5516   E cep 5521   We wwe 5574   × cxp 5620  dom cdm 5622   ↾ cres 5624  Ord word 6314  Oncon0 6315  ‘cfv 6490   ≼ cdom 8882  OrdIsocoi 9415

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 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7315  df-ov 7361  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-en 8885  df-dom 8886  df-oi 9416

This theorem is referenced by:  card2on  9460  harf  9464  harval  9466