Metamath Proof Explorer

Theorem onintunirab

Description: The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion onintunirab ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
2 ssint ⊢ ( 𝑥 ⊆ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
3 1 2 sylibr ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → 𝑥 ⊆ ∩ 𝐴 )
4 simp2 ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → 𝑥 ∈ On )
5 oninton ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )
6 5 3ad2ant1 ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → ∩ 𝐴 ∈ On )
7 onsssuc ⊢ ( ( 𝑥 ∈ On ∧ ∩ 𝐴 ∈ On ) → ( 𝑥 ⊆ ∩ 𝐴 ↔ 𝑥 ∈ suc ∩ 𝐴 ) )
8 4 6 7 syl2anc ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → ( 𝑥 ⊆ ∩ 𝐴 ↔ 𝑥 ∈ suc ∩ 𝐴 ) )
9 3 8 mpbid ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → 𝑥 ∈ suc ∩ 𝐴 )
10 9 rabssdv ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ suc ∩ 𝐴 )
11 ssrab2 ⊢ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ On
12 11 a1i ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ On )
13 eloni ⊢ ( ∩ 𝐴 ∈ On → Ord ∩ 𝐴 )
14 5 13 syl ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → Ord ∩ 𝐴 )
15 ordunisssuc ⊢ ( ( { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ On ∧ Ord ∩ 𝐴 ) → ( ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ ∩ 𝐴 ↔ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ suc ∩ 𝐴 ) )
16 12 14 15 syl2anc ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ ∩ 𝐴 ↔ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ suc ∩ 𝐴 ) )
17 10 16 mpbird ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ ∩ 𝐴 )
18 sseq1 ⊢ ( 𝑥 = ∩ 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ ∩ 𝐴 ⊆ 𝑦 ) )
19 18 ralbidv ⊢ ( 𝑥 = ∩ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ∩ 𝐴 ⊆ 𝑦 ) )
20 intss1 ⊢ ( 𝑦 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑦 )
21 20 rgen ⊢ ∀ 𝑦 ∈ 𝐴 ∩ 𝐴 ⊆ 𝑦
22 21 a1i ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∀ 𝑦 ∈ 𝐴 ∩ 𝐴 ⊆ 𝑦 )
23 19 5 22 elrabd ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )
24 unissel ⊢ ( ( ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ ∩ 𝐴 ∧ ∩ 𝐴 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ) → ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } = ∩ 𝐴 )
25 17 23 24 syl2anc ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } = ∩ 𝐴 )
26 25 eqcomd ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )