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 ( 𝑥𝐵𝐶 ) ≼ ω )