Step | Hyp | Ref
| Expression |
1 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (𝑥 <s 𝑧 ↔ 𝑋 <s 𝑧)) |
2 | 1 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) ↔ (𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦))) |
3 | 2 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴))) |
4 | 3 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴))) |
5 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑌 → (𝑧 <s 𝑦 ↔ 𝑧 <s 𝑌)) |
6 | 5 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) ↔ (𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌))) |
7 | 6 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → (((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴))) |
8 | 7 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) ↔ ∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴))) |
9 | 4, 8 | rspc2v 3293 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) → ∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴))) |
10 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑋 <s 𝑧 ↔ 𝑋 <s 𝑤)) |
11 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑧 <s 𝑌 ↔ 𝑤 <s 𝑌)) |
12 | 10, 11 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) ↔ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
13 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
14 | 12, 13 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) ↔ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → 𝑤 ∈ 𝐴))) |
15 | 14 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈
No → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → 𝑤 ∈ 𝐴))) |
16 | | bdaydm 31077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom bday = No
|
17 | 16 | sseq2i 3593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ⊆ dom bday ↔ 𝐴 ⊆ No
) |
18 | | bdayfun 31075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Fun bday |
19 | | funfvima2 6397 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
bday ∧ 𝐴 ⊆ dom bday
) → (𝑤 ∈
𝐴 → ( bday ‘𝑤) ∈ ( bday
“ 𝐴))) |
20 | 18, 19 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ⊆ dom bday → (𝑤 ∈ 𝐴 → ( bday
‘𝑤) ∈
( bday “ 𝐴))) |
21 | 17, 20 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆
No → (𝑤 ∈
𝐴 → ( bday ‘𝑤) ∈ ( bday
“ 𝐴))) |
22 | 21 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ( bday ‘𝑤) ∈ ( bday
“ 𝐴)) |
23 | | intss1 4427 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( bday ‘𝑤) ∈ ( bday
“ 𝐴) → ∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤)) |
25 | | imassrn 5396 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( bday “ 𝐴) ⊆ ran bday
|
26 | | bdayrn 31076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ran bday = On |
27 | 25, 26 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( bday “ 𝐴) ⊆ On |
28 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (( bday ‘𝑤) ∈ ( bday
“ 𝐴) → ( bday “ 𝐴) ≠ ∅) |
29 | 22, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ( bday “ 𝐴) ≠ ∅) |
30 | | oninton 6892 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((( bday “ 𝐴) ⊆ On ∧ (
bday “ 𝐴)
≠ ∅) → ∩ ( bday
“ 𝐴) ∈
On) |
31 | 27, 29, 30 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ∩ ( bday “ 𝐴) ∈ On) |
32 | | bdayelon 31079 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( bday ‘𝑤) ∈ On |
33 | | ontri1 5674 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((∩ ( bday “ 𝐴) ∈ On ∧ ( bday ‘𝑤) ∈ On) → (∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤) ↔ ¬ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
34 | 31, 32, 33 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → (∩ ( bday “ 𝐴) ⊆ ( bday ‘𝑤) ↔ ¬ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
35 | 24, 34 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆
No ∧ 𝑤 ∈
𝐴) → ¬ ( bday ‘𝑤) ∈ ∩ ( bday “ 𝐴)) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆
No → (𝑤 ∈
𝐴 → ¬ ( bday ‘𝑤) ∈ ∩ ( bday “ 𝐴))) |
37 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) → (( bday
‘𝑤) ∈
( bday ‘𝑋) ↔ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
38 | 37 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) → (¬ ( bday
‘𝑤) ∈
( bday ‘𝑋) ↔ ¬ ( bday
‘𝑤) ∈
∩ ( bday “ 𝐴))) |
39 | 38 | biimprcd 239 |
. . . . . . . . . . . . . . . 16
⊢ (¬
( bday ‘𝑤) ∈ ∩ ( bday “ 𝐴) → (( bday
‘𝑋) = ∩ ( bday “ 𝐴) → ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋))) |
40 | 36, 39 | syl6 34 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆
No → (𝑤 ∈
𝐴 → (( bday ‘𝑋) = ∩ ( bday “ 𝐴) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))) |
41 | 40 | com3l 87 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝐴 → (( bday
‘𝑋) = ∩ ( bday “ 𝐴) → (𝐴 ⊆ No
→ ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)))) |
42 | 41 | adantrd 483 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐴 → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝐴 ⊆ No
→ ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)))) |
43 | 15, 42 | syl8 74 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈
No → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝐴 ⊆ No
→ ¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)))))) |
44 | 43 | com35 96 |
. . . . . . . . . . 11
⊢ (𝑤 ∈
No → (∀𝑧 ∈ No
((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))))) |
45 | 44 | com4l 90 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
No ((𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))))) |
46 | 9, 45 | syl6 34 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋))))))) |
47 | 46 | com3l 87 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴) → (𝐴 ⊆ No
→ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋))))))) |
48 | 47 | impcom 445 |
. . . . . . 7
⊢ ((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)) → (𝑤 ∈ No
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋)))))) |
49 | 48 | imp42 618 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑤 ∈ No )
→ ((𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) → ¬ ( bday
‘𝑤) ∈
( bday ‘𝑋))) |
50 | 49 | con2d 128 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑤 ∈ No )
→ (( bday ‘𝑤) ∈ ( bday
‘𝑋) →
¬ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
51 | | 3anass 1035 |
. . . . . . 7
⊢ ((( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) ↔ (( bday
‘𝑤) ∈
( bday ‘𝑋) ∧ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
52 | 51 | notbii 309 |
. . . . . 6
⊢ (¬
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) ↔ ¬ (( bday
‘𝑤) ∈
( bday ‘𝑋) ∧ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
53 | | imnan 437 |
. . . . . 6
⊢ ((( bday ‘𝑤) ∈ ( bday
‘𝑋) →
¬ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) ↔ ¬ ((
bday ‘𝑤)
∈ ( bday ‘𝑋) ∧ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
54 | 52, 53 | bitr4i 266 |
. . . . 5
⊢ (¬
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌) ↔ (( bday
‘𝑤) ∈
( bday ‘𝑋) → ¬ (𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌))) |
55 | 50, 54 | sylibr 223 |
. . . 4
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑤 ∈ No )
→ ¬ (( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
56 | 55 | nrexdv 2984 |
. . 3
⊢ (((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ¬ ∃𝑤 ∈
No (( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
57 | | ssel 3562 |
. . . . . . . . 9
⊢ (𝐴 ⊆
No → (𝑋 ∈
𝐴 → 𝑋 ∈ No
)) |
58 | | ssel 3562 |
. . . . . . . . 9
⊢ (𝐴 ⊆
No → (𝑌 ∈
𝐴 → 𝑌 ∈ No
)) |
59 | 57, 58 | anim12d 584 |
. . . . . . . 8
⊢ (𝐴 ⊆
No → ((𝑋
∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∈ No
∧ 𝑌 ∈ No ))) |
60 | 59 | imp 444 |
. . . . . . 7
⊢ ((𝐴 ⊆
No ∧ (𝑋 ∈
𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋 ∈ No
∧ 𝑌 ∈ No )) |
61 | | eqtr3 2631 |
. . . . . . 7
⊢ ((( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday
‘𝑌) = ∩ ( bday “ 𝐴)) → ( bday ‘𝑋) = ( bday
‘𝑌)) |
62 | 60, 61 | anim12i 588 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ (𝑋 ∈
𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌))) |
63 | 62 | anasss 677 |
. . . . 5
⊢ ((𝐴 ⊆
No ∧ ((𝑋 ∈
𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌))) |
64 | 63 | adantlr 747 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌))) |
65 | | nodense 31088 |
. . . . 5
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ) ∧ (( bday
‘𝑋) = ( bday ‘𝑌) ∧ 𝑋 <s 𝑌)) → ∃𝑤 ∈ No
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
66 | 65 | anassrs 678 |
. . . 4
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ) ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ∃𝑤 ∈ No
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
67 | 64, 66 | sylan 487 |
. . 3
⊢ ((((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) ∧ 𝑋 <s 𝑌) → ∃𝑤 ∈ No
(( bday ‘𝑤) ∈ ( bday
‘𝑋) ∧
𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌)) |
68 | 56, 67 | mtand 689 |
. 2
⊢ (((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴)))) → ¬ 𝑋 <s 𝑌) |
69 | 68 | ex 449 |
1
⊢ ((𝐴 ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday
‘𝑋) = ∩ ( bday “ 𝐴) ∧ (
bday ‘𝑌) =
∩ ( bday “ 𝐴))) → ¬ 𝑋 <s 𝑌)) |