Theorem onintrab

Description: The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003)

	Ref	Expression
Assertion	onintrab	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )

Proof

Step	Hyp	Ref	Expression
1		intex	⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V )
2		ssrab2	⊢ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On
3		oninton	⊢ ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )
4	2 3	mpan	⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )
5	1 4	sylbir	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )
6		elex	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V )
7	5 6	impbii	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )