This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ‘ 𝑥 ) ⊆ ( 𝐵 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ‘ 𝑥 ) )
2 smofvon ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ 𝐴 ) ∈ On )
3 smoel ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝐴 ) )
4 3 3expia ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝐴 ) ) )
5 ontr1 ⊢ ( ( 𝐵 ‘ 𝐴 ) ∈ On → ( ( 𝑦 ∈ ( 𝐵 ‘ 𝑥 ) ∧ ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝐴 ) ) → 𝑦 ∈ ( 𝐵 ‘ 𝐴 ) ) )
6 5 expcomd ⊢ ( ( 𝐵 ‘ 𝐴 ) ∈ On → ( ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝐴 ) → ( 𝑦 ∈ ( 𝐵 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
7 2 4 6 sylsyld ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ ( 𝐵 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
8 7 rexlimdv ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐵 ‘ 𝐴 ) ) )
9 1 8 biimtrid ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐵 ‘ 𝐴 ) ) )
10 9 ssrdv ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ‘ 𝑥 ) ⊆ ( 𝐵 ‘ 𝐴 ) )