Step |
Hyp |
Ref |
Expression |
1 |
|
psrbag0.d |
⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
2 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
3 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
4 |
2 3
|
ifcli |
⊢ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ0 |
5 |
4
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ0 ) |
6 |
5
|
fmpttd |
⊢ ( ⊤ → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 ) |
7 |
6
|
mptru |
⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 |
8 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) |
9 |
8
|
mptpreima |
⊢ ( ◡ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) = { 𝑥 ∈ 𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } |
10 |
|
snfi |
⊢ { 𝐾 } ∈ Fin |
11 |
|
inss1 |
⊢ ( { 𝑥 ∣ 𝑥 = 𝐾 } ∩ 𝐼 ) ⊆ { 𝑥 ∣ 𝑥 = 𝐾 } |
12 |
|
dfrab2 |
⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } = ( { 𝑥 ∣ 𝑥 = 𝐾 } ∩ 𝐼 ) |
13 |
|
df-sn |
⊢ { 𝐾 } = { 𝑥 ∣ 𝑥 = 𝐾 } |
14 |
11 12 13
|
3sstr4i |
⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } ⊆ { 𝐾 } |
15 |
|
ssfi |
⊢ ( ( { 𝐾 } ∈ Fin ∧ { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } ⊆ { 𝐾 } ) → { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } ∈ Fin ) |
16 |
10 14 15
|
mp2an |
⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } ∈ Fin |
17 |
|
0nnn |
⊢ ¬ 0 ∈ ℕ |
18 |
|
iffalse |
⊢ ( ¬ 𝑥 = 𝐾 → if ( 𝑥 = 𝐾 , 1 , 0 ) = 0 ) |
19 |
18
|
eleq1d |
⊢ ( ¬ 𝑥 = 𝐾 → ( if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ ↔ 0 ∈ ℕ ) ) |
20 |
17 19
|
mtbiri |
⊢ ( ¬ 𝑥 = 𝐾 → ¬ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ ) |
21 |
20
|
con4i |
⊢ ( if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ → 𝑥 = 𝐾 ) |
22 |
21
|
a1i |
⊢ ( 𝑥 ∈ 𝐼 → ( if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ → 𝑥 = 𝐾 ) ) |
23 |
22
|
ss2rabi |
⊢ { 𝑥 ∈ 𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ⊆ { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } |
24 |
|
ssfi |
⊢ ( ( { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } ∈ Fin ∧ { 𝑥 ∈ 𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ⊆ { 𝑥 ∈ 𝐼 ∣ 𝑥 = 𝐾 } ) → { 𝑥 ∈ 𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ∈ Fin ) |
25 |
16 23 24
|
mp2an |
⊢ { 𝑥 ∈ 𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ∈ Fin |
26 |
9 25
|
eqeltri |
⊢ ( ◡ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) ∈ Fin |
27 |
7 26
|
pm3.2i |
⊢ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) ∈ Fin ) |
28 |
1
|
psrbag |
⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) ∈ Fin ) ) ) |
29 |
27 28
|
mpbiri |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) ∈ 𝐷 ) |