Step | Hyp | Ref
| Expression |
1 | | bdayelon 33971 |
. . . . . . . . . 10
⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On |
2 | 1 | onssneli 6376 |
. . . . . . . . 9
⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday
‘𝑥) →
¬ ( bday ‘𝑥) ∈ ( bday
‘(𝐴 |s 𝐵))) |
3 | | leftssold 34061 |
. . . . . . . . . . . . 13
⊢ ( L
‘𝑋) ⊆ ( O
‘( bday ‘𝑋)) |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ ( O ‘(
bday ‘𝑋))) |
5 | 4 | sselda 3921 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ ( O ‘(
bday ‘𝑋))) |
6 | | bdayelon 33971 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑋) ∈ On |
7 | | leftssno 34063 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑋) ⊆ No |
8 | 7 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ No
) |
9 | 8 | sselda 3921 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ No
) |
10 | | oldbday 34081 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑥 ∈ No )
→ (𝑥 ∈ ( O
‘( bday ‘𝑋)) ↔ ( bday
‘𝑥) ∈
( bday ‘𝑋))) |
11 | 6, 9, 10 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (𝑥 ∈ ( O ‘(
bday ‘𝑋))
↔ ( bday ‘𝑥) ∈ ( bday
‘𝑋))) |
12 | 5, 11 | mpbid 231 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday
‘𝑥) ∈
( bday ‘𝑋)) |
13 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵)) |
14 | 13 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday
‘𝑋) = ( bday ‘(𝐴 |s 𝐵))) |
15 | 12, 14 | eleqtrd 2841 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday
‘𝑥) ∈
( bday ‘(𝐴 |s 𝐵))) |
16 | 2, 15 | nsyl3 138 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥)) |
17 | | scutbday 33998 |
. . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
18 | 17 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
19 | | bdayfn 33968 |
. . . . . . . . . . 11
⊢ bday Fn No
|
20 | | ssrab2 4013 |
. . . . . . . . . . 11
⊢ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
|
21 | | sneq 4571 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑥 → {𝑡} = {𝑥}) |
22 | 21 | breq2d 5086 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑥 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑥})) |
23 | 21 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑥 → ({𝑡} <<s 𝐵 ↔ {𝑥} <<s 𝐵)) |
24 | 22, 23 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
25 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ No
) |
26 | | snex 5354 |
. . . . . . . . . . . . . . 15
⊢ {𝑥} ∈ V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ∈ V) |
28 | | ssltex2 33982 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ∈ V) |
30 | 9 | snssd 4742 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ⊆ No
) |
31 | | ssltss2 33984 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
32 | 31 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ⊆ No
) |
33 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 ∈ No
) |
34 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 = (𝐴 |s 𝐵)) |
35 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵) |
36 | 35 | scutcld 33997 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝐴 |s 𝐵) ∈ No
) |
37 | 34, 36 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 ∈ No
) |
38 | 37 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 ∈ No
) |
39 | 32 | sselda 3921 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No
) |
40 | | leftval 34047 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( L
‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋}) |
42 | 41 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋})) |
43 | | rabid 3310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋)) |
44 | 42, 43 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋))) |
45 | 44 | simplbda 500 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 <s 𝑋) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑋) |
47 | | simpllr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵)) |
48 | | scutcut 33995 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
49 | 48 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
50 | 49 | simp3d 1143 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {(𝐴 |s 𝐵)} <<s 𝐵) |
51 | | ovex 7308 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 |s 𝐵) ∈ V |
52 | 51 | snid 4597 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} |
53 | | ssltsepc 33987 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏) |
54 | 52, 53 | mp3an2 1448 |
. . . . . . . . . . . . . . . . . . 19
⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏) |
55 | 50, 54 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏) |
56 | 47, 55 | eqbrtrd 5096 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 <s 𝑏) |
57 | 33, 38, 39, 46, 56 | slttrd 33962 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏) |
58 | 57 | 3adant2 1130 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏) |
59 | | velsn 4577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ {𝑥} ↔ 𝑎 = 𝑥) |
60 | | breq1 5077 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑥 → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏)) |
61 | 59, 60 | sylbi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ {𝑥} → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏)) |
62 | 61 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏)) |
63 | 58, 62 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏) |
64 | 27, 29, 30, 32, 63 | ssltd 33986 |
. . . . . . . . . . . . 13
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} <<s 𝐵) |
65 | 64 | anim1ci 616 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)) |
66 | 24, 25, 65 | elrabd 3626 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) |
67 | | fnfvima 7109 |
. . . . . . . . . . 11
⊢ (( bday Fn No ∧ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
∧ 𝑥 ∈ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday
‘𝑥) ∈
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
68 | 19, 20, 66, 67 | mp3an12i 1464 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday
‘𝑥) ∈
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
69 | | intss1 4894 |
. . . . . . . . . 10
⊢ (( bday ‘𝑥) ∈ ( bday
“ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday
‘𝑥)) |
70 | 68, 69 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ∩ ( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday
‘𝑥)) |
71 | 18, 70 | eqsstrd 3959 |
. . . . . . . 8
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥)) |
72 | 16, 71 | mtand 813 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ 𝐴 <<s {𝑥}) |
73 | | ssltex1 33981 |
. . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
74 | 73 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ∈ V) |
75 | 74, 26 | jctir 521 |
. . . . . . . 8
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ∈ V ∧ {𝑥} ∈ V)) |
76 | | ssltss1 33983 |
. . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
77 | 76 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ⊆ No
) |
78 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝑥 ∈ No
) |
79 | 78 | snssd 4742 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → {𝑥} ⊆ No
) |
80 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) |
81 | 77, 79, 80 | 3jca 1127 |
. . . . . . . 8
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ⊆ No
∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)) |
82 | | brsslt 33980 |
. . . . . . . 8
⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆ No
∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡))) |
83 | 75, 81, 82 | sylanbrc 583 |
. . . . . . 7
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 <<s {𝑥}) |
84 | 72, 83 | mtand 813 |
. . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) |
85 | | rexnal 3169 |
. . . . . . 7
⊢
(∃𝑡 ∈
{𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡) |
86 | | ralcom 3166 |
. . . . . . 7
⊢
(∀𝑡 ∈
{𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) |
87 | 85, 86 | xchbinx 334 |
. . . . . 6
⊢
(∃𝑡 ∈
{𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) |
88 | 84, 87 | sylibr 233 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡) |
89 | | vex 3436 |
. . . . . 6
⊢ 𝑥 ∈ V |
90 | | breq2 5078 |
. . . . . . . 8
⊢ (𝑡 = 𝑥 → (𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥)) |
91 | 90 | ralbidv 3112 |
. . . . . . 7
⊢ (𝑡 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)) |
92 | 91 | notbid 318 |
. . . . . 6
⊢ (𝑡 = 𝑥 → (¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)) |
93 | 89, 92 | rexsn 4618 |
. . . . 5
⊢
(∃𝑡 ∈
{𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥) |
94 | 88, 93 | sylib 217 |
. . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥) |
95 | 76 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐴 ⊆ No
) |
96 | 95 | sselda 3921 |
. . . . . . 7
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No
) |
97 | | slenlt 33955 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥)) |
98 | 9, 96, 97 | syl2an2r 682 |
. . . . . 6
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥)) |
99 | 98 | rexbidva 3225 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥)) |
100 | | rexnal 3169 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 ¬ 𝑦 <s 𝑥 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥) |
101 | 99, 100 | bitrdi 287 |
. . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)) |
102 | 94, 101 | mpbird 256 |
. . 3
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) |
103 | 102 | ralrimiva 3103 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) |
104 | 1 | onssneli 6376 |
. . . . . . . . 9
⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday
‘𝑧) →
¬ ( bday ‘𝑧) ∈ ( bday
‘(𝐴 |s 𝐵))) |
105 | | rightssold 34062 |
. . . . . . . . . . . . 13
⊢ ( R
‘𝑋) ⊆ ( O
‘( bday ‘𝑋)) |
106 | 105 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ ( O ‘(
bday ‘𝑋))) |
107 | 106 | sselda 3921 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ ( O ‘(
bday ‘𝑋))) |
108 | | rightssno 34064 |
. . . . . . . . . . . . . 14
⊢ ( R
‘𝑋) ⊆ No |
109 | 108 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ No
) |
110 | 109 | sselda 3921 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ No
) |
111 | | oldbday 34081 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑧 ∈ No )
→ (𝑧 ∈ ( O
‘( bday ‘𝑋)) ↔ ( bday
‘𝑧) ∈
( bday ‘𝑋))) |
112 | 6, 110, 111 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (𝑧 ∈ ( O ‘(
bday ‘𝑋))
↔ ( bday ‘𝑧) ∈ ( bday
‘𝑋))) |
113 | 107, 112 | mpbid 231 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday
‘𝑧) ∈
( bday ‘𝑋)) |
114 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵)) |
115 | 114 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday
‘𝑋) = ( bday ‘(𝐴 |s 𝐵))) |
116 | 113, 115 | eleqtrd 2841 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday
‘𝑧) ∈
( bday ‘(𝐴 |s 𝐵))) |
117 | 104, 116 | nsyl3 138 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧)) |
118 | 17 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
119 | | sneq 4571 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧}) |
120 | 119 | breq2d 5086 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑧})) |
121 | 119 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → ({𝑡} <<s 𝐵 ↔ {𝑧} <<s 𝐵)) |
122 | 120, 121 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑧 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))) |
123 | 110 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ No
) |
124 | 73 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ∈ V) |
125 | | snex 5354 |
. . . . . . . . . . . . . . 15
⊢ {𝑧} ∈ V |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ∈ V) |
127 | 76 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ⊆ No
) |
128 | 110 | snssd 4742 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ⊆ No
) |
129 | 127 | sselda 3921 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No
) |
130 | 37 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 ∈ No
) |
131 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ No
) |
132 | 48 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
133 | 132 | simp2d 1142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {(𝐴 |s 𝐵)}) |
134 | | ssltsepc 33987 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) → 𝑎 <s (𝐴 |s 𝐵)) |
135 | 52, 134 | mp3an3 1449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵)) |
136 | 133, 135 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵)) |
137 | | simpllr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵)) |
138 | 136, 137 | breqtrrd 5102 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑋) |
139 | | rightval 34048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( R
‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}) |
141 | 140 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧})) |
142 | | rabid 3310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑧)) |
143 | 141, 142 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ (𝑧 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑧))) |
144 | 143 | simplbda 500 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 <s 𝑧) |
145 | 144 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 <s 𝑧) |
146 | 129, 130,
131, 138, 145 | slttrd 33962 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑧) |
147 | 146 | 3adant3 1131 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑧) |
148 | | velsn 4577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ {𝑧} ↔ 𝑏 = 𝑧) |
149 | | breq2 5078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑧 → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧)) |
150 | 148, 149 | sylbi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ {𝑧} → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧)) |
151 | 150 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧)) |
152 | 147, 151 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑏) |
153 | 124, 126,
127, 128, 152 | ssltd 33986 |
. . . . . . . . . . . . 13
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {𝑧}) |
154 | 153 | anim1i 615 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)) |
155 | 122, 123,
154 | elrabd 3626 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) |
156 | | fnfvima 7109 |
. . . . . . . . . . 11
⊢ (( bday Fn No ∧ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
∧ 𝑧 ∈ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday
‘𝑧) ∈
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
157 | 19, 20, 155, 156 | mp3an12i 1464 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday
‘𝑧) ∈
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
158 | | intss1 4894 |
. . . . . . . . . 10
⊢ (( bday ‘𝑧) ∈ ( bday
“ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday
‘𝑧)) |
159 | 157, 158 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ∩ ( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday
‘𝑧)) |
160 | 118, 159 | eqsstrd 3959 |
. . . . . . . 8
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧)) |
161 | 117, 160 | mtand 813 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ {𝑧} <<s 𝐵) |
162 | 28 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ∈ V) |
163 | 162, 125 | jctil 520 |
. . . . . . . 8
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ∈ V ∧ 𝐵 ∈ V)) |
164 | 128 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} ⊆ No
) |
165 | 31 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ⊆ No
) |
166 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) |
167 | 164, 165,
166 | 3jca 1127 |
. . . . . . . 8
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ⊆ No
∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)) |
168 | | brsslt 33980 |
. . . . . . . 8
⊢ ({𝑧} <<s 𝐵 ↔ (({𝑧} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑧} ⊆ No
∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤))) |
169 | 163, 167,
168 | sylanbrc 583 |
. . . . . . 7
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} <<s 𝐵) |
170 | 161, 169 | mtand 813 |
. . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) |
171 | | rexnal 3169 |
. . . . . 6
⊢
(∃𝑡 ∈
{𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) |
172 | 170, 171 | sylibr 233 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) |
173 | | vex 3436 |
. . . . . 6
⊢ 𝑧 ∈ V |
174 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑡 = 𝑧 → (𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤)) |
175 | 174 | ralbidv 3112 |
. . . . . . 7
⊢ (𝑡 = 𝑧 → (∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)) |
176 | 175 | notbid 318 |
. . . . . 6
⊢ (𝑡 = 𝑧 → (¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)) |
177 | 173, 176 | rexsn 4618 |
. . . . 5
⊢
(∃𝑡 ∈
{𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤) |
178 | 172, 177 | sylib 217 |
. . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤) |
179 | 31 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐵 ⊆ No
) |
180 | 179 | sselda 3921 |
. . . . . . 7
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No
) |
181 | 110 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ No
) |
182 | | slenlt 33955 |
. . . . . . 7
⊢ ((𝑤 ∈
No ∧ 𝑧 ∈
No ) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤)) |
183 | 180, 181,
182 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤)) |
184 | 183 | rexbidva 3225 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤)) |
185 | | rexnal 3169 |
. . . . 5
⊢
(∃𝑤 ∈
𝐵 ¬ 𝑧 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤) |
186 | 184, 185 | bitrdi 287 |
. . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)) |
187 | 178, 186 | mpbird 256 |
. . 3
⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧) |
188 | 187 | ralrimiva 3103 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧) |
189 | 103, 188 | jca 512 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)) |