Step | Hyp | Ref
| Expression |
1 | | ssltex1 33614 |
. . 3
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
2 | | ssltss1 33616 |
. . 3
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
3 | 1, 2 | elpwd 4493 |
. 2
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ 𝒫 No
) |
4 | | df-br 5028 |
. . . 4
⊢ (𝐴 <<s 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ <<s ) |
5 | 4 | biimpi 219 |
. . 3
⊢ (𝐴 <<s 𝐵 → 〈𝐴, 𝐵〉 ∈ <<s ) |
6 | | ssltex2 33615 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
7 | | elimasng 5923 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵 ∈ ( <<s “
{𝐴}) ↔ 〈𝐴, 𝐵〉 ∈ <<s )) |
8 | 1, 6, 7 | syl2anc 587 |
. . 3
⊢ (𝐴 <<s 𝐵 → (𝐵 ∈ ( <<s “ {𝐴}) ↔ 〈𝐴, 𝐵〉 ∈ <<s )) |
9 | 5, 8 | mpbird 260 |
. 2
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ ( <<s “ {𝐴})) |
10 | | riotaex 7125 |
. . 3
⊢
(℩𝑥
∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) ∈ V |
11 | | breq1 5030 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎 <<s {𝑦} ↔ 𝐴 <<s {𝑦})) |
12 | | breq2 5031 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ({𝑦} <<s 𝑏 ↔ {𝑦} <<s 𝐵)) |
13 | 11, 12 | bi2anan9 639 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏) ↔ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))) |
14 | 13 | rabbidv 3380 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} = {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
15 | 14 | imaeq2d 5897 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ( bday
“ {𝑦 ∈
No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}) = ( bday
“ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
16 | 15 | inteqd 4838 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∩ ( bday “ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
17 | 16 | eqeq2d 2749 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}) ↔ ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
18 | 14, 17 | riotaeqbidv 7124 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
19 | | sneq 4523 |
. . . . 5
⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴}) |
20 | 19 | imaeq2d 5897 |
. . . 4
⊢ (𝑎 = 𝐴 → ( <<s “ {𝑎}) = ( <<s “ {𝐴})) |
21 | | df-scut 33611 |
. . . 4
⊢ |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
22 | 18, 20, 21 | ovmpox 7312 |
. . 3
⊢ ((𝐴 ∈ 𝒫 No ∧ 𝐵 ∈ ( <<s “ {𝐴}) ∧ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) ∈ V) → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
23 | 10, 22 | mp3an3 1451 |
. 2
⊢ ((𝐴 ∈ 𝒫 No ∧ 𝐵 ∈ ( <<s “ {𝐴})) → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
24 | 3, 9, 23 | syl2anc 587 |
1
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |