Description: If for every element of a set of ordinals there is an element of a subset which is at least as large, then the union of the set and the subset is the same. Lemma 2.12 of Schloeder p. 5. (Contributed by RP, 27-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | onsssupeqcond | ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 ) → ∪ 𝐴 = ∪ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uniss2 | ⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 → ∪ 𝐴 ⊆ ∪ 𝐵 ) | |
| 2 | 1 | adantl | ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 ) → ∪ 𝐴 ⊆ ∪ 𝐵 ) |
| 3 | uniss | ⊢ ( 𝐵 ⊆ 𝐴 → ∪ 𝐵 ⊆ ∪ 𝐴 ) | |
| 4 | 3 | adantr | ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 ) → ∪ 𝐵 ⊆ ∪ 𝐴 ) |
| 5 | 2 4 | eqssd | ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 ) → ∪ 𝐴 = ∪ 𝐵 ) |
| 6 | 5 | a1i | ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 ) → ∪ 𝐴 = ∪ 𝐵 ) ) |