Step |
Hyp |
Ref |
Expression |
1 |
|
psrbag.d |
⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
2 |
|
df-rab |
⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) } |
3 |
1
|
psrbag |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑦 ∈ 𝐷 ↔ ( 𝑦 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑦 “ ℕ ) ∈ Fin ) ) ) |
4 |
3
|
adantr |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ↔ ( 𝑦 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑦 “ ℕ ) ∈ Fin ) ) ) |
5 |
|
simpl |
⊢ ( ( 𝑦 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑦 “ ℕ ) ∈ Fin ) → 𝑦 : 𝐼 ⟶ ℕ0 ) |
6 |
4 5
|
syl6bi |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 → 𝑦 : 𝐼 ⟶ ℕ0 ) ) |
7 |
6
|
adantrd |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) → 𝑦 : 𝐼 ⟶ ℕ0 ) ) |
8 |
|
ss2ixp |
⊢ ( ∀ 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ ℕ0 → X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ 𝐼 ℕ0 ) |
9 |
|
fz0ssnn0 |
⊢ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ ℕ0 |
10 |
9
|
a1i |
⊢ ( 𝑥 ∈ 𝐼 → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ ℕ0 ) |
11 |
8 10
|
mprg |
⊢ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ 𝐼 ℕ0 |
12 |
11
|
sseli |
⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ X 𝑥 ∈ 𝐼 ℕ0 ) |
13 |
|
vex |
⊢ 𝑦 ∈ V |
14 |
13
|
elixpconst |
⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ℕ0 ↔ 𝑦 : 𝐼 ⟶ ℕ0 ) |
15 |
12 14
|
sylib |
⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) → 𝑦 : 𝐼 ⟶ ℕ0 ) |
16 |
15
|
a1i |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) → 𝑦 : 𝐼 ⟶ ℕ0 ) ) |
17 |
|
ffn |
⊢ ( 𝑦 : 𝐼 ⟶ ℕ0 → 𝑦 Fn 𝐼 ) |
18 |
17
|
adantl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝑦 Fn 𝐼 ) |
19 |
13
|
elixp |
⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) |
20 |
19
|
baib |
⊢ ( 𝑦 Fn 𝐼 → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) |
21 |
18 20
|
syl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) |
22 |
|
ffvelrn |
⊢ ( ( 𝑦 : 𝐼 ⟶ ℕ0 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ℕ0 ) |
23 |
22
|
adantll |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ℕ0 ) |
24 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
25 |
23 24
|
eleqtrdi |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) ) |
26 |
1
|
psrbagfOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 ) |
27 |
26
|
adantr |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝐹 : 𝐼 ⟶ ℕ0 ) |
28 |
27
|
ffvelrnda |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 ) |
29 |
28
|
nn0zd |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ ) |
30 |
|
elfz5 |
⊢ ( ( ( 𝑦 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℤ ) → ( ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
31 |
25 29 30
|
syl2anc |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
32 |
31
|
ralbidva |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
33 |
27
|
ffnd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝐹 Fn 𝐼 ) |
34 |
|
simpll |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝐼 ∈ 𝑉 ) |
35 |
|
inidm |
⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼 |
36 |
|
eqidd |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) = ( 𝑦 ‘ 𝑥 ) ) |
37 |
|
eqidd |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
38 |
18 33 34 34 35 36 37
|
ofrfval |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
39 |
32 38
|
bitr4d |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ 𝑦 ∘r ≤ 𝐹 ) ) |
40 |
1
|
psrbagleclOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∘r ≤ 𝐹 ) ) → 𝑦 ∈ 𝐷 ) |
41 |
40
|
3exp2 |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ∈ 𝐷 → ( 𝑦 : 𝐼 ⟶ ℕ0 → ( 𝑦 ∘r ≤ 𝐹 → 𝑦 ∈ 𝐷 ) ) ) ) |
42 |
41
|
imp31 |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∘r ≤ 𝐹 → 𝑦 ∈ 𝐷 ) ) |
43 |
42
|
pm4.71rd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ) ) |
44 |
21 39 43
|
3bitrrd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ↔ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) |
45 |
44
|
ex |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑦 : 𝐼 ⟶ ℕ0 → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ↔ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) ) |
46 |
7 16 45
|
pm5.21ndd |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ↔ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) |
47 |
46
|
abbi1dv |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) } = X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) |
48 |
2 47
|
syl5eq |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } = X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) |
49 |
|
simpr |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 ∈ 𝐷 ) |
50 |
|
cnveq |
⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 ) |
51 |
50
|
imaeq1d |
⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝐹 “ ℕ ) ) |
52 |
51
|
eleq1d |
⊢ ( 𝑓 = 𝐹 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) |
53 |
52 1
|
elrab2 |
⊢ ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) |
54 |
49 53
|
sylib |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) |
55 |
54
|
simprd |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( ◡ 𝐹 “ ℕ ) ∈ Fin ) |
56 |
|
fzfid |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ∈ Fin ) |
57 |
|
simpl |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 ) |
58 |
57 26
|
jca |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) ) |
59 |
|
frnnn0supp |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) ) |
60 |
|
eqimss |
⊢ ( ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) ) |
61 |
58 59 60
|
3syl |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) ) |
62 |
|
c0ex |
⊢ 0 ∈ V |
63 |
62
|
a1i |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 0 ∈ V ) |
64 |
26 61 57 63
|
suppssr |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 ) |
65 |
64
|
oveq2d |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) = ( 0 ... 0 ) ) |
66 |
|
fz0sn |
⊢ ( 0 ... 0 ) = { 0 } |
67 |
65 66
|
eqtrdi |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) = { 0 } ) |
68 |
|
eqimss |
⊢ ( ( 0 ... ( 𝐹 ‘ 𝑥 ) ) = { 0 } → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ { 0 } ) |
69 |
67 68
|
syl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ { 0 } ) |
70 |
55 56 69
|
ixpfi2 |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ∈ Fin ) |
71 |
48 70
|
eqeltrd |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin ) |