Step |
Hyp |
Ref |
Expression |
1 |
|
etasslt |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) |
2 |
|
simpl1 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s 𝐵 ) |
3 |
|
scutbday |
⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
4 |
2 3
|
syl |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
5 |
|
bdayfn |
⊢ bday Fn No |
6 |
|
ssrab2 |
⊢ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No |
7 |
|
sneq |
⊢ ( 𝑦 = 𝑥 → { 𝑦 } = { 𝑥 } ) |
8 |
7
|
breq2d |
⊢ ( 𝑦 = 𝑥 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑥 } ) ) |
9 |
7
|
breq1d |
⊢ ( 𝑦 = 𝑥 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑥 } <<s 𝐵 ) ) |
10 |
8 9
|
anbi12d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) |
11 |
|
simprl |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝑥 ∈ No ) |
12 |
|
simprr1 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s { 𝑥 } ) |
13 |
|
simprr2 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → { 𝑥 } <<s 𝐵 ) |
14 |
12 13
|
jca |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) |
15 |
10 11 14
|
elrabd |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) |
16 |
|
fnfvima |
⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No ∧ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
17 |
5 6 15 16
|
mp3an12i |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
18 |
|
intss1 |
⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) ) |
19 |
17 18
|
syl |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) ) |
20 |
4 19
|
eqsstrd |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑥 ) ) |
21 |
|
simprr3 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ 𝑥 ) ⊆ 𝑂 ) |
22 |
20 21
|
sstrd |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 ) |
23 |
1 22
|
rexlimddv |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 ) |