Theorem onintonm 4550

Description: The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.)

Assertion

Ref	Expression
onintonm	⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ On)

Distinct variable group:   𝑥,𝐴

Proof of Theorem onintonm

Step	Hyp	Ref	Expression
1		ssel 3174	. . . . . . 7 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
2		eloni 4407	. . . . . . . 8 ⊢ (𝑥 ∈ On → Ord 𝑥)
3		ordtr 4410	. . . . . . . 8 ⊢ (Ord 𝑥 → Tr 𝑥)
4	2, 3	syl 14	. . . . . . 7 ⊢ (𝑥 ∈ On → Tr 𝑥)
5	1, 4	syl6 33	. . . . . 6 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → Tr 𝑥))
6	5	ralrimiv 2566	. . . . 5 ⊢ (𝐴 ⊆ On → ∀𝑥 ∈ 𝐴 Tr 𝑥)
7		trint 4143	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
8	6, 7	syl 14	. . . 4 ⊢ (𝐴 ⊆ On → Tr ∩ 𝐴)
9	8	adantr 276	. . 3 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → Tr ∩ 𝐴)
10		nfv 1539	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ⊆ On
11		nfe1 1507	. . . . 5 ⊢ Ⅎ𝑥∃𝑥 𝑥 ∈ 𝐴
12	10, 11	nfan 1576	. . . 4 ⊢ Ⅎ𝑥(𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴)
13		intssuni2m 3895	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ On)
14		unon 4544	. . . . . . . 8 ⊢ ∪ On = On
15	13, 14	sseqtrdi 3228	. . . . . . 7 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ On)
16	15	sseld 3179	. . . . . 6 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ On))
17	16, 2	syl6 33	. . . . 5 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (𝑥 ∈ ∩ 𝐴 → Ord 𝑥))
18	17, 3	syl6 33	. . . 4 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (𝑥 ∈ ∩ 𝐴 → Tr 𝑥))
19	12, 18	ralrimi 2565	. . 3 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∀𝑥 ∈ ∩ 𝐴Tr 𝑥)
20		dford3 4399	. . 3 ⊢ (Ord ∩ 𝐴 ↔ (Tr ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴Tr 𝑥))
21	9, 19, 20	sylanbrc 417	. 2 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → Ord ∩ 𝐴)
22		inteximm 4179	. . . 4 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
23	22	adantl 277	. . 3 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ V)
24		elong 4405	. . 3 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ On ↔ Ord ∩ 𝐴))
25	23, 24	syl 14	. 2 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (∩ 𝐴 ∈ On ↔ Ord ∩ 𝐴))
26	21, 25	mpbird 167	1 ⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∃wex 1503   ∈ wcel 2164  ∀wral 2472  Vcvv 2760   ⊆ wss 3154  ∪ cuni 3836  ∩ cint 3871  Tr wtr 4128  Ord word 4394  Oncon0 4395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-uni 3837  df-int 3872  df-tr 4129  df-iord 4398  df-on 4400  df-suc 4403

This theorem is referenced by:  onintrab2im  4551