Description: The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of BellMachover p. 471. (Contributed by NM, 20-Sep-2003)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | uniordint.1 | ⊢ 𝐴 ∈ V | |
| Assertion | uniordint | ⊢ ( 𝐴 ⊆ On → ∪ 𝐴 = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uniordint.1 | ⊢ 𝐴 ∈ V | |
| 2 | 1 | ssonunii | ⊢ ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) |
| 3 | intmin | ⊢ ( ∪ 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ ∪ 𝐴 ⊆ 𝑥 } = ∪ 𝐴 ) | |
| 4 | unissb | ⊢ ( ∪ 𝐴 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) | |
| 5 | 4 | rabbii | ⊢ { 𝑥 ∈ On ∣ ∪ 𝐴 ⊆ 𝑥 } = { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 } |
| 6 | 5 | inteqi | ⊢ ∩ { 𝑥 ∈ On ∣ ∪ 𝐴 ⊆ 𝑥 } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 } |
| 7 | 3 6 | eqtr3di | ⊢ ( ∪ 𝐴 ∈ On → ∪ 𝐴 = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 } ) |
| 8 | 2 7 | syl | ⊢ ( 𝐴 ⊆ On → ∪ 𝐴 = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 } ) |