| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (𝑥 <s 𝑧 ↔ 𝑋 <s 𝑧)) |
| 2 | 1 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) ↔ (𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦))) |
| 3 | 2 | imbi1d 341 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴))) |
| 4 | 3 | ralbidv 3178 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴))) |
| 5 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑌 → (𝑧 <s 𝑦 ↔ 𝑧 <s 𝑌)) |
| 6 | 5 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) ↔ (𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌))) |
| 7 | 6 | imbi1d 341 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → (((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴))) |
| 8 | 7 | ralbidv 3178 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴))) |
| 9 | 4, 8 | rspc2v 3633 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) → ∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴))) |
| 10 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑋 <s 𝑧 ↔ 𝑋 <s 𝑤)) |
| 11 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑧 <s 𝑌 ↔ 𝑤 <s 𝑌)) |
| 12 | 10, 11 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) ↔ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
| 13 | | eleq1w 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
| 14 | 12, 13 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) ↔ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → 𝑤 ∈ 𝐴))) |
| 15 | 14 | rspcv 3618 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈
No → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → 𝑤 ∈ 𝐴))) |
| 16 | | bdaydm 27819 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom bday = No
|
| 17 | 16 | sseq2i 4013 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ⊆ dom bday ↔ 𝐴 ⊆ No
) |
| 18 | | bdayfun 27817 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Fun bday |
| 19 | | funfvima2 7251 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
bday ∧ 𝐴 ⊆ dom bday
) → (𝑤 ∈
𝐴 → ( bday ‘𝑤) ∈ ( bday
“ 𝐴))) |
| 20 | 18, 19 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ⊆ dom bday → (𝑤 ∈ 𝐴 → ( bday
‘𝑤) ∈
( bday “ 𝐴))) |
| 21 | 17, 20 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆
No → (𝑤 ∈
𝐴 → ( bday ‘𝑤) ∈ ( bday
“ 𝐴))) |
| 22 | 21 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ( bday ‘𝑤) ∈ ( bday
“ 𝐴)) |
| 23 | | intss1 4963 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( bday ‘𝑤) ∈ ( bday
“ 𝐴) → ∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤)) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤)) |
| 25 | | imassrn 6089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( bday “ 𝐴) ⊆ ran bday
|
| 26 | | bdayrn 27820 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ran bday = On |
| 27 | 25, 26 | sseqtri 4032 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( bday “ 𝐴) ⊆ On |
| 28 | 22 | ne0d 4342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ( bday “ 𝐴) ≠ ∅) |
| 29 | | oninton 7815 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((( bday “ 𝐴) ⊆ On ∧ (
bday “ 𝐴)
≠ ∅) → ∩ ( bday
“ 𝐴) ∈
On) |
| 30 | 27, 28, 29 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ∩ ( bday “ 𝐴) ∈ On) |
| 31 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( bday ‘𝑤) ∈ On |
| 32 | | ontri1 6418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((∩ ( bday “ 𝐴) ∈ On ∧ ( bday ‘𝑤) ∈ On) → (∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤) ↔ ¬ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
| 33 | 30, 31, 32 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → (∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤) ↔ ¬ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
| 34 | 24, 33 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ¬ ( bday ‘𝑤) ∈ ∩ ( bday “ 𝐴)) |
| 35 | 34 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆
No → (𝑤 ∈
𝐴 → ¬ ( bday ‘𝑤) ∈ ∩ ( bday “ 𝐴))) |
| 36 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) → (( bday
‘𝑤) ∈
( bday ‘𝑋) ↔ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
| 37 | 36 | notbid 318 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) → (¬ ( bday
‘𝑤) ∈
( bday ‘𝑋) ↔ ¬ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
| 38 | 37 | biimprcd 250 |
. . . . . . . . . . . . . . . 16
⊢ (¬
( bday ‘𝑤) ∈ ∩ ( bday “ 𝐴) → (( bday
‘𝑋) = ∩ ( bday “ 𝐴) → ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋))) |
| 39 | 35, 38 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆
No → (𝑤 ∈
𝐴 → (( bday ‘𝑋) = ∩ ( bday “ 𝐴) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))) |
| 40 | 39 | com3l 89 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝐴 → (( bday
‘𝑋) = ∩ ( bday “ 𝐴) → (𝐴 ⊆ No
→ ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)))) |
| 41 | 40 | adantrd 491 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐴 → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝐴 ⊆ No
→ ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)))) |
| 42 | 15, 41 | syl8 76 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈
No → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝐴 ⊆ No
→ ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)))))) |
| 43 | 42 | com35 98 |
. . . . . . . . . . 11
⊢ (𝑤 ∈
No → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))))) |
| 44 | 43 | com4l 92 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
No ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))))) |
| 45 | 9, 44 | syl6 35 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋))))))) |
| 46 | 45 | com3l 89 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋))))))) |
| 47 | 46 | impcom 407 |
. . . . . . 7
⊢ ((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))))) |
| 48 | 47 | imp42 426 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑤 ∈ No )
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋))) |
| 49 | 48 | con2d 134 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑤 ∈ No )
→ (( bday ‘𝑤) ∈ ( bday
‘𝑋) →
¬ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
| 50 | | 3anass 1095 |
. . . . . . 7
⊢ ((( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) ↔ (( bday
‘𝑤) ∈
( bday ‘𝑋) ∧ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
| 51 | 50 | notbii 320 |
. . . . . 6
⊢ (¬
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) ↔ ¬ (( bday
‘𝑤) ∈
( bday ‘𝑋) ∧ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
| 52 | | imnan 399 |
. . . . . 6
⊢ ((( bday ‘𝑤) ∈ ( bday
‘𝑋) →
¬ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) ↔ ¬ ((
bday ‘𝑤)
∈ ( bday ‘𝑋) ∧ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
| 53 | 51, 52 | bitr4i 278 |
. . . . 5
⊢ (¬
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) ↔ (( bday
‘𝑤) ∈
( bday ‘𝑋) → ¬ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
| 54 | 49, 53 | sylibr 234 |
. . . 4
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑤 ∈ No )
→ ¬ (( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
| 55 | 54 | nrexdv 3149 |
. . 3
⊢ (((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ¬ ∃𝑤 ∈
No (( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
| 56 | | ssel 3977 |
. . . . . . . . 9
⊢ (𝐴 ⊆
No → (𝑋 ∈
𝐴 → 𝑋 ∈ No
)) |
| 57 | | ssel 3977 |
. . . . . . . . 9
⊢ (𝐴 ⊆
No → (𝑌 ∈
𝐴 → 𝑌 ∈ No
)) |
| 58 | 56, 57 | anim12d 609 |
. . . . . . . 8
⊢ (𝐴 ⊆
No → ((𝑋
∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∈ No
∧ 𝑌 ∈ No ))) |
| 59 | 58 | imp 406 |
. . . . . . 7
⊢ ((𝐴 ⊆
No ∧ (𝑋 ∈
𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋 ∈ No
∧ 𝑌 ∈ No )) |
| 60 | | eqtr3 2763 |
. . . . . . 7
⊢ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → ( bday ‘𝑋) = ( bday
‘𝑌)) |
| 61 | 59, 60 | anim12i 613 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ (𝑋 ∈
𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌))) |
| 62 | 61 | anasss 466 |
. . . . 5
⊢ ((𝐴 ⊆
No ∧ ((𝑋 ∈
𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌))) |
| 63 | 62 | adantlr 715 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌))) |
| 64 | | nodense 27737 |
. . . . 5
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ) ∧ (( bday
‘𝑋) = ( bday ‘𝑌) ∧ 𝑋 <s 𝑌)) → ∃𝑤 ∈ No
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
| 65 | 64 | anassrs 467 |
. . . 4
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ∃𝑤 ∈ No
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
| 66 | 63, 65 | sylan 580 |
. . 3
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑋 <s 𝑌) → ∃𝑤 ∈ No
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
| 67 | 55, 66 | mtand 816 |
. 2
⊢ (((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ¬ 𝑋 <s 𝑌) |
| 68 | 67 | ex 412 |
1
⊢ ((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴))) → ¬ 𝑋 <s 𝑌)) |