Metamath Proof Explorer

Theorem 1stcrestlem

Description: Lemma for 1stcrest . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion 1stcrestlem ⊢B≼ω→ran⁡x∈B⟼C≼ω

Proof

Step Hyp Ref Expression
1 ordom ⊢Ord⁡ω
2 reldom ⊢Rel⁡≼
3 2 brrelex2i ⊢B≼ω→ω∈V
4 elong ⊢ω∈V→ω∈On↔Ord⁡ω
5 3 4 syl ⊢B≼ω→ω∈On↔Ord⁡ω
6 1 5 mpbiri ⊢B≼ω→ω∈On
7 ondomen ⊢ω∈On∧B≼ω→B∈dom⁡card
8 6 7 mpancom ⊢B≼ω→B∈dom⁡card
9 eqid ⊢x∈B⟼C=x∈B⟼C
10 9 dmmptss ⊢dom⁡x∈B⟼C⊆B
11 ssnum ⊢B∈dom⁡card∧dom⁡x∈B⟼C⊆B→dom⁡x∈B⟼C∈dom⁡card
12 8 10 11 sylancl ⊢B≼ω→dom⁡x∈B⟼C∈dom⁡card
13 funmpt ⊢Fun⁡x∈B⟼C
14 funforn ⊢Fun⁡x∈B⟼C↔x∈B⟼C:dom⁡x∈B⟼C⟶ontoran⁡x∈B⟼C
15 13 14 mpbi ⊢x∈B⟼C:dom⁡x∈B⟼C⟶ontoran⁡x∈B⟼C
16 fodomnum ⊢dom⁡x∈B⟼C∈dom⁡card→x∈B⟼C:dom⁡x∈B⟼C⟶ontoran⁡x∈B⟼C→ran⁡x∈B⟼C≼dom⁡x∈B⟼C
17 12 15 16 mpisyl ⊢B≼ω→ran⁡x∈B⟼C≼dom⁡x∈B⟼C
18 ctex ⊢B≼ω→B∈V
19 ssdomg ⊢B∈V→dom⁡x∈B⟼C⊆B→dom⁡x∈B⟼C≼B
20 18 10 19 mpisyl ⊢B≼ω→dom⁡x∈B⟼C≼B
21 domtr ⊢dom⁡x∈B⟼C≼B∧B≼ω→dom⁡x∈B⟼C≼ω
22 20 21 mpancom ⊢B≼ω→dom⁡x∈B⟼C≼ω
23 domtr ⊢ran⁡x∈B⟼C≼dom⁡x∈B⟼C∧dom⁡x∈B⟼C≼ω→ran⁡x∈B⟼C≼ω
24 17 22 23 syl2anc ⊢B≼ω→ran⁡x∈B⟼C≼ω