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 ⟶ onto ran ⁡ x ∈ B ⟼ C
15 13 14 mpbi ⊢ x ∈ B ⟼ C : dom ⁡ x ∈ B ⟼ C ⟶ onto ran ⁡ x ∈ B ⟼ C
16 fodomnum ⊢ dom ⁡ x ∈ B ⟼ C ∈ dom ⁡ card → x ∈ B ⟼ C : dom ⁡ x ∈ B ⟼ C ⟶ onto ran ⁡ 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 ≼ ω