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

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 ( 𝐵 ≼ ω → ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ≼ ω )

Proof

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