Step |
Hyp |
Ref |
Expression |
1 |
|
df-scut |
⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) |
2 |
1
|
mpofun |
⊢ Fun |s |
3 |
|
dmscut |
⊢ dom |s = <<s |
4 |
|
df-fn |
⊢ ( |s Fn <<s ↔ ( Fun |s ∧ dom |s = <<s ) ) |
5 |
2 3 4
|
mpbir2an |
⊢ |s Fn <<s |
6 |
1
|
rnmpo |
⊢ ran |s = { 𝑧 ∣ ∃ 𝑎 ∈ 𝒫 No ∃ 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) } |
7 |
|
vex |
⊢ 𝑎 ∈ V |
8 |
|
vex |
⊢ 𝑏 ∈ V |
9 |
7 8
|
elimasn |
⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ 〈 𝑎 , 𝑏 〉 ∈ <<s ) |
10 |
|
df-br |
⊢ ( 𝑎 <<s 𝑏 ↔ 〈 𝑎 , 𝑏 〉 ∈ <<s ) |
11 |
9 10
|
bitr4i |
⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ 𝑎 <<s 𝑏 ) |
12 |
|
scutval |
⊢ ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) |
13 |
|
scutcl |
⊢ ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) ∈ No ) |
14 |
12 13
|
eqeltrrd |
⊢ ( 𝑎 <<s 𝑏 → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No ) |
15 |
11 14
|
sylbi |
⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No ) |
16 |
|
eleq1a |
⊢ ( ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No → ( 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) ) |
17 |
15 16
|
syl |
⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) → ( 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) ) |
18 |
17
|
adantl |
⊢ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) → ( 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) ) |
19 |
18
|
rexlimivv |
⊢ ( ∃ 𝑎 ∈ 𝒫 No ∃ 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) |
20 |
19
|
abssi |
⊢ { 𝑧 ∣ ∃ 𝑎 ∈ 𝒫 No ∃ 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) } ⊆ No |
21 |
6 20
|
eqsstri |
⊢ ran |s ⊆ No |
22 |
|
df-f |
⊢ ( |s : <<s ⟶ No ↔ ( |s Fn <<s ∧ ran |s ⊆ No ) ) |
23 |
5 21 22
|
mpbir2an |
⊢ |s : <<s ⟶ No |