Theorem onint

Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of TakeutiZaring p. 45. (Contributed by NM, 31-Jan-1997)

	Ref	Expression
Assertion	onint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ordon	⊢ Ord On
2		tz7.5	⊢ ( ( Ord On ∧ 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
3	1 2	mp3an1	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
4		ssel	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On ) )
5	4	imdistani	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) )
6		ssel	⊢ ( 𝐴 ⊆ On → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ On ) )
7		ontri1	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑥 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑥 ) )
8		ssel	⊢ ( 𝑥 ⊆ 𝑧 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
9	7 8	syl6bir	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ¬ 𝑧 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) )
10	9	ex	⊢ ( 𝑥 ∈ On → ( 𝑧 ∈ On → ( ¬ 𝑧 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
11	6 10	sylan9	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ 𝐴 → ( ¬ 𝑧 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
12	11	com4r	⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ 𝐴 → ( ¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
13	12	imp31	⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
14	13	ralimdva	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) ) → ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 → ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 ) )
15		disj	⊢ ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 )
16		vex	⊢ 𝑦 ∈ V
17	16	elint2	⊢ ( 𝑦 ∈ ∩ 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 )
18	14 15 17	3imtr4g	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) ) → ( ( 𝐴 ∩ 𝑥 ) = ∅ → 𝑦 ∈ ∩ 𝐴 ) )
19	5 18	sylan2	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝐴 ∩ 𝑥 ) = ∅ → 𝑦 ∈ ∩ 𝐴 ) )
20	19	exp32	⊢ ( 𝑦 ∈ 𝑥 → ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → 𝑦 ∈ ∩ 𝐴 ) ) ) )
21	20	com4l	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴 ) ) ) )
22	21	imp32	⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴 ) )
23	22	ssrdv	⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → 𝑥 ⊆ ∩ 𝐴 )
24		intss1	⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥 )
25	24	ad2antrl	⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ∩ 𝐴 ⊆ 𝑥 )
26	23 25	eqssd	⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → 𝑥 = ∩ 𝐴 )
27	26	eleq1d	⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ( 𝑥 ∈ 𝐴 ↔ ∩ 𝐴 ∈ 𝐴 ) )
28	27	biimpd	⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴 ) )
29	28	exp32	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴 ) ) ) )
30	29	com34	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ∩ 𝐴 ∈ 𝐴 ) ) ) )
31	30	pm2.43d	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ∩ 𝐴 ∈ 𝐴 ) ) )
32	31	rexlimdv	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ → ∩ 𝐴 ∈ 𝐴 ) )
33	3 32	syl5	⊢ ( 𝐴 ⊆ On → ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 ) )
34	33	anabsi5	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )