Metamath Proof Explorer

Theorem smoiun

Description: The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011)

Ref Expression
Assertion smoiun ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → ⋃ x ∈ A B ⁡ x ⊆ B ⁡ A

Proof

Step Hyp Ref Expression
1 eliun ⊢ y ∈ ⋃ x ∈ A B ⁡ x ↔ ∃ x ∈ A y ∈ B ⁡ x
2 smofvon ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → B ⁡ A ∈ On
3 smoel ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B ∧ x ∈ A → B ⁡ x ∈ B ⁡ A
4 3 3expia ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → x ∈ A → B ⁡ x ∈ B ⁡ A
5 ontr1 ⊢ B ⁡ A ∈ On → y ∈ B ⁡ x ∧ B ⁡ x ∈ B ⁡ A → y ∈ B ⁡ A
6 5 expcomd ⊢ B ⁡ A ∈ On → B ⁡ x ∈ B ⁡ A → y ∈ B ⁡ x → y ∈ B ⁡ A
7 2 4 6 sylsyld ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → x ∈ A → y ∈ B ⁡ x → y ∈ B ⁡ A
8 7 rexlimdv ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → ∃ x ∈ A y ∈ B ⁡ x → y ∈ B ⁡ A
9 1 8 syl5bi ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → y ∈ ⋃ x ∈ A B ⁡ x → y ∈ B ⁡ A
10 9 ssrdv ⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → ⋃ x ∈ A B ⁡ x ⊆ B ⁡ A