Step |
Hyp |
Ref |
Expression |
1 |
|
ssltex1 |
⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V ) |
2 |
|
ssltss1 |
⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No ) |
3 |
1 2
|
elpwd |
⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ 𝒫 No ) |
4 |
|
df-br |
⊢ ( 𝐴 <<s 𝐵 ↔ 〈 𝐴 , 𝐵 〉 ∈ <<s ) |
5 |
4
|
biimpi |
⊢ ( 𝐴 <<s 𝐵 → 〈 𝐴 , 𝐵 〉 ∈ <<s ) |
6 |
|
ssltex2 |
⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V ) |
7 |
|
elimasng |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ ( <<s “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐵 〉 ∈ <<s ) ) |
8 |
1 6 7
|
syl2anc |
⊢ ( 𝐴 <<s 𝐵 → ( 𝐵 ∈ ( <<s “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐵 〉 ∈ <<s ) ) |
9 |
5 8
|
mpbird |
⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ ( <<s “ { 𝐴 } ) ) |
10 |
|
riotaex |
⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ∈ V |
11 |
|
breq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑦 } ) ) |
12 |
|
breq2 |
⊢ ( 𝑏 = 𝐵 → ( { 𝑦 } <<s 𝑏 ↔ { 𝑦 } <<s 𝐵 ) ) |
13 |
11 12
|
bi2anan9 |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) ↔ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ) ) |
14 |
13
|
rabbidv |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } = { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) |
15 |
14
|
imaeq2d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) = ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
16 |
15
|
inteqd |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
17 |
16
|
eqeq2d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ↔ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
18 |
14 17
|
riotaeqbidv |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
19 |
|
sneq |
⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } ) |
20 |
19
|
imaeq2d |
⊢ ( 𝑎 = 𝐴 → ( <<s “ { 𝑎 } ) = ( <<s “ { 𝐴 } ) ) |
21 |
|
df-scut |
⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) |
22 |
18 20 21
|
ovmpox |
⊢ ( ( 𝐴 ∈ 𝒫 No ∧ 𝐵 ∈ ( <<s “ { 𝐴 } ) ∧ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ∈ V ) → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
23 |
10 22
|
mp3an3 |
⊢ ( ( 𝐴 ∈ 𝒫 No ∧ 𝐵 ∈ ( <<s “ { 𝐴 } ) ) → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
24 |
3 9 23
|
syl2anc |
⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |