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