Step | Hyp | Ref
| Expression |
1 | | simp2l 1201 |
. . . . 5
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝐴 <<s {𝑋}) |
2 | | simp2r 1202 |
. . . . 5
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → {𝑋} <<s 𝐵) |
3 | | snnzg 4707 |
. . . . . 6
⊢ (𝑋 ∈
No → {𝑋} ≠
∅) |
4 | 3 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → {𝑋} ≠ ∅) |
5 | | sslttr 33772 |
. . . . 5
⊢ ((𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵 ∧ {𝑋} ≠ ∅) → 𝐴 <<s 𝐵) |
6 | 1, 2, 4, 5 | syl3anc 1373 |
. . . 4
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵) |
7 | | scutbday 33769 |
. . . 4
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
8 | 6, 7 | syl 17 |
. . 3
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
9 | | bdayfn 33739 |
. . . . 5
⊢ bday Fn No
|
10 | | ssrab2 4010 |
. . . . 5
⊢ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
|
11 | | simp1 1138 |
. . . . . 6
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝑋 ∈ No
) |
12 | | simp2 1139 |
. . . . . 6
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵)) |
13 | | sneq 4568 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → {𝑦} = {𝑋}) |
14 | 13 | breq2d 5082 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑋})) |
15 | 13 | breq1d 5080 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → ({𝑦} <<s 𝐵 ↔ {𝑋} <<s 𝐵)) |
16 | 14, 15 | anbi12d 634 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵))) |
17 | 16 | elrab 3617 |
. . . . . 6
⊢ (𝑋 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑋 ∈ No
∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵))) |
18 | 11, 12, 17 | sylanbrc 586 |
. . . . 5
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → 𝑋 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
19 | | fnfvima 7071 |
. . . . 5
⊢ (( bday Fn No ∧ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
∧ 𝑋 ∈ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday
‘𝑋) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
20 | 9, 10, 18, 19 | mp3an12i 1467 |
. . . 4
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday
‘𝑋) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
21 | | intss1 4891 |
. . . 4
⊢ (( bday ‘𝑋) ∈ ( bday
“ {𝑦 ∈
No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑋)) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑋)) |
23 | 8, 22 | eqsstrd 3956 |
. 2
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑋)) |
24 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → 𝐴 <<s {𝑋}) |
25 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → {𝑋} <<s 𝐵) |
26 | 3 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → {𝑋} ≠ ∅) |
27 | 24, 25, 26, 5 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → 𝐴 <<s 𝐵) |
28 | 27, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
29 | 28 | eqeq1d 2741 |
. . . . . . . . 9
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋)
↔ ∩ ( bday
“ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) = ( bday
‘𝑋))) |
30 | | eqcom 2746 |
. . . . . . . . 9
⊢ (∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) = ( bday
‘𝑋) ↔
( bday ‘𝑋) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
31 | 29, 30 | bitrdi 290 |
. . . . . . . 8
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋)
↔ ( bday ‘𝑋) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
32 | 31 | biimpa 480 |
. . . . . . 7
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ ( bday ‘𝑋) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
33 | 17 | biimpri 231 |
. . . . . . . 8
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → 𝑋 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
34 | 27 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ 𝐴 <<s 𝐵) |
35 | | conway 33764 |
. . . . . . . . 9
⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ ∃!𝑥 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
37 | | fveqeq2 6748 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ( bday
‘𝑋) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
38 | 37 | riota2 7218 |
. . . . . . . . 9
⊢ ((𝑋 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ∧ ∃!𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) → (( bday
‘𝑋) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) = 𝑋)) |
39 | | eqcom 2746 |
. . . . . . . . 9
⊢
((℩𝑥
∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) = 𝑋 ↔ 𝑋 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
40 | 38, 39 | bitrdi 290 |
. . . . . . . 8
⊢ ((𝑋 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ∧ ∃!𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) → (( bday
‘𝑋) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ 𝑋 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})))) |
41 | 33, 36, 40 | syl2an2r 685 |
. . . . . . 7
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ (( bday ‘𝑋) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ 𝑋 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})))) |
42 | 32, 41 | mpbid 235 |
. . . . . 6
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ 𝑋 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
43 | | scutval 33765 |
. . . . . . 7
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
44 | 34, 43 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) |
45 | 42, 44 | eqtr4d 2782 |
. . . . 5
⊢ (((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋))
→ 𝑋 = (𝐴 |s 𝐵)) |
46 | 45 | ex 416 |
. . . 4
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (( bday
‘(𝐴 |s 𝐵)) = (
bday ‘𝑋)
→ 𝑋 = (𝐴 |s 𝐵))) |
47 | 46 | necon3d 2964 |
. . 3
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵)) → (𝑋 ≠ (𝐴 |s 𝐵) → ( bday
‘(𝐴 |s 𝐵)) ≠ (
bday ‘𝑋))) |
48 | 47 | 3impia 1119 |
. 2
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday
‘(𝐴 |s 𝐵)) ≠ (
bday ‘𝑋)) |
49 | | bdayelon 33742 |
. . 3
⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On |
50 | | bdayelon 33742 |
. . 3
⊢ ( bday ‘𝑋) ∈ On |
51 | | onelpss 6274 |
. . 3
⊢ ((( bday ‘(𝐴 |s 𝐵)) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday
‘𝑋) ↔
(( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday
‘𝑋) ∧
( bday ‘(𝐴 |s 𝐵)) ≠ ( bday
‘𝑋)))) |
52 | 49, 50, 51 | mp2an 692 |
. 2
⊢ (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday
‘𝑋) ↔
(( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday
‘𝑋) ∧
( bday ‘(𝐴 |s 𝐵)) ≠ ( bday
‘𝑋))) |
53 | 23, 48, 52 | sylanbrc 586 |
1
⊢ ((𝑋 ∈
No ∧ (𝐴
<<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday
‘(𝐴 |s 𝐵)) ∈ ( bday ‘𝑋)) |