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