Step | Hyp | Ref
| Expression |
1 | | ssltss1 33979 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
2 | | ssltex1 33977 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
3 | | ssltss2 33980 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
4 | | ssltex2 33978 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
5 | | ssltsep 33981 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐵 𝑝 <s 𝑞) |
6 | | noeta2 33975 |
. . . . 5
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐵 𝑝 <s 𝑞) → ∃𝑦 ∈ No
(∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday
‘𝑦) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
7 | 1, 2, 3, 4, 5, 6 | syl221anc 1380 |
. . . 4
⊢ (𝐴 <<s 𝐵 → ∃𝑦 ∈ No
(∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday
‘𝑦) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
8 | | 3simpa 1147 |
. . . . . 6
⊢
((∀𝑝 ∈
𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday
‘𝑦) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) → (∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞)) |
9 | 2 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → 𝐴 ∈ V) |
10 | | snex 5358 |
. . . . . . . . . 10
⊢ {𝑦} ∈ V |
11 | 9, 10 | jctir 521 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → (𝐴 ∈ V ∧ {𝑦} ∈ V)) |
12 | 1 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → 𝐴 ⊆ No
) |
13 | | snssi 4747 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
No → {𝑦}
⊆ No ) |
14 | 13 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
→ {𝑦} ⊆ No ) |
15 | 14 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → {𝑦} ⊆ No
) |
16 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
17 | | breq2 5083 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑦 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑦)) |
18 | 16, 17 | ralsn 4623 |
. . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
{𝑦}𝑝 <s 𝑞 ↔ 𝑝 <s 𝑦) |
19 | 18 | ralbii 3093 |
. . . . . . . . . . . 12
⊢
(∀𝑝 ∈
𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞 ↔ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) |
20 | 19 | biimpri 227 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
𝐴 𝑝 <s 𝑦 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞) |
21 | 20 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞) |
22 | 12, 15, 21 | 3jca 1127 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → (𝐴 ⊆ No
∧ {𝑦} ⊆ No ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞)) |
23 | | brsslt 33976 |
. . . . . . . . 9
⊢ (𝐴 <<s {𝑦} ↔ ((𝐴 ∈ V ∧ {𝑦} ∈ V) ∧ (𝐴 ⊆ No
∧ {𝑦} ⊆ No ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞))) |
24 | 11, 22, 23 | sylanbrc 583 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑝 ∈
𝐴 𝑝 <s 𝑦) → 𝐴 <<s {𝑦}) |
25 | 24 | ex 413 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
→ (∀𝑝 ∈
𝐴 𝑝 <s 𝑦 → 𝐴 <<s {𝑦})) |
26 | 4 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → 𝐵 ∈ V) |
27 | 26, 10 | jctil 520 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → ({𝑦} ∈ V ∧ 𝐵 ∈ V)) |
28 | 14 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → {𝑦} ⊆ No
) |
29 | 3 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → 𝐵 ⊆ No
) |
30 | | ralcom 3283 |
. . . . . . . . . . . 12
⊢
(∀𝑝 ∈
{𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞 ↔ ∀𝑞 ∈ 𝐵 ∀𝑝 ∈ {𝑦}𝑝 <s 𝑞) |
31 | | breq1 5082 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑦 → (𝑝 <s 𝑞 ↔ 𝑦 <s 𝑞)) |
32 | 16, 31 | ralsn 4623 |
. . . . . . . . . . . . 13
⊢
(∀𝑝 ∈
{𝑦}𝑝 <s 𝑞 ↔ 𝑦 <s 𝑞) |
33 | 32 | ralbii 3093 |
. . . . . . . . . . . 12
⊢
(∀𝑞 ∈
𝐵 ∀𝑝 ∈ {𝑦}𝑝 <s 𝑞 ↔ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) |
34 | 30, 33 | sylbbr 235 |
. . . . . . . . . . 11
⊢
(∀𝑞 ∈
𝐵 𝑦 <s 𝑞 → ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞) |
35 | 34 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞) |
36 | 28, 29, 35 | 3jca 1127 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → ({𝑦} ⊆ No
∧ 𝐵 ⊆ No ∧ ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞)) |
37 | | brsslt 33976 |
. . . . . . . . 9
⊢ ({𝑦} <<s 𝐵 ↔ (({𝑦} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑦} ⊆ No
∧ 𝐵 ⊆ No ∧ ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞))) |
38 | 27, 36, 37 | sylanbrc 583 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
∧ ∀𝑞 ∈
𝐵 𝑦 <s 𝑞) → {𝑦} <<s 𝐵) |
39 | 38 | ex 413 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
→ (∀𝑞 ∈
𝐵 𝑦 <s 𝑞 → {𝑦} <<s 𝐵)) |
40 | 25, 39 | anim12d 609 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
→ ((∀𝑝 ∈
𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))) |
41 | 8, 40 | syl5 34 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No )
→ ((∀𝑝 ∈
𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday
‘𝑦) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) → (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))) |
42 | 41 | reximdva 3205 |
. . . 4
⊢ (𝐴 <<s 𝐵 → (∃𝑦 ∈ No
(∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday
‘𝑦) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) → ∃𝑦 ∈ No
(𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))) |
43 | 7, 42 | mpd 15 |
. . 3
⊢ (𝐴 <<s 𝐵 → ∃𝑦 ∈ No
(𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)) |
44 | | rabn0 4325 |
. . 3
⊢ ({𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ≠ ∅ ↔ ∃𝑦 ∈
No (𝐴 <<s
{𝑦} ∧ {𝑦} <<s 𝐵)) |
45 | 43, 44 | sylibr 233 |
. 2
⊢ (𝐴 <<s 𝐵 → {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ≠ ∅) |
46 | | ssrab2 4018 |
. . 3
⊢ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
|
47 | 46 | a1i 11 |
. 2
⊢ (𝐴 <<s 𝐵 → {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
) |
48 | | simplr3 1216 |
. . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑟 ∈ No
) |
49 | 2 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 ∈ V) |
50 | | snex 5358 |
. . . . . . . 8
⊢ {𝑟} ∈ V |
51 | 49, 50 | jctir 521 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → (𝐴 ∈ V ∧ {𝑟} ∈ V)) |
52 | 1 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 ⊆ No
) |
53 | | snssi 4747 |
. . . . . . . . 9
⊢ (𝑟 ∈
No → {𝑟}
⊆ No ) |
54 | 48, 53 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → {𝑟} ⊆ No
) |
55 | 52 | sselda 3926 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ No
) |
56 | | simplr1 1214 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑝 ∈ No
) |
57 | 56 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑝 ∈ No
) |
58 | 48 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ No
) |
59 | | simplll 772 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞)) → 𝐴 <<s {𝑝}) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 <<s {𝑝}) |
61 | | ssltsep 33981 |
. . . . . . . . . . . . . 14
⊢ (𝐴 <<s {𝑝} → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑝}𝑥 <s 𝑦) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑝}𝑥 <s 𝑦) |
63 | 62 | r19.21bi 3135 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑝}𝑥 <s 𝑦) |
64 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑝 ∈ V |
65 | | breq2 5083 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑝 → (𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝)) |
66 | 64, 65 | ralsn 4623 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
{𝑝}𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝) |
67 | 63, 66 | sylib 217 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s 𝑝) |
68 | | simprrl 778 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑝 <s 𝑟) |
69 | 68 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑝 <s 𝑟) |
70 | 55, 57, 58, 67, 69 | slttrd 33958 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s 𝑟) |
71 | | vex 3435 |
. . . . . . . . . . 11
⊢ 𝑟 ∈ V |
72 | | breq2 5083 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑟 → (𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟)) |
73 | 71, 72 | ralsn 4623 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
{𝑟}𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟) |
74 | 70, 73 | sylibr 233 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦) |
75 | 74 | ralrimiva 3110 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦) |
76 | 52, 54, 75 | 3jca 1127 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → (𝐴 ⊆ No
∧ {𝑟} ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦)) |
77 | | brsslt 33976 |
. . . . . . 7
⊢ (𝐴 <<s {𝑟} ↔ ((𝐴 ∈ V ∧ {𝑟} ∈ V) ∧ (𝐴 ⊆ No
∧ {𝑟} ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦))) |
78 | 51, 76, 77 | sylanbrc 583 |
. . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 <<s {𝑟}) |
79 | 4 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐵 ∈ V) |
80 | 79, 50 | jctil 520 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ({𝑟} ∈ V ∧ 𝐵 ∈ V)) |
81 | 3 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐵 ⊆ No
) |
82 | 48 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑟 ∈ No
) |
83 | | simplr2 1215 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑞 ∈ No
) |
84 | 83 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑞 ∈ No
) |
85 | 81 | sselda 3926 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ No
) |
86 | | simprrr 779 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑟 <s 𝑞) |
87 | 86 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑟 <s 𝑞) |
88 | | simplrr 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞)) → {𝑞} <<s 𝐵) |
89 | 88 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → {𝑞} <<s 𝐵) |
90 | | ssltsep 33981 |
. . . . . . . . . . . . . 14
⊢ ({𝑞} <<s 𝐵 → ∀𝑥 ∈ {𝑞}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ {𝑞}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
92 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑞 ∈ V |
93 | | breq1 5082 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → (𝑥 <s 𝑦 ↔ 𝑞 <s 𝑦)) |
94 | 93 | ralbidv 3123 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑞 <s 𝑦)) |
95 | 92, 94 | ralsn 4623 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{𝑞}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑞 <s 𝑦) |
96 | 91, 95 | sylib 217 |
. . . . . . . . . . . 12
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑦 ∈ 𝐵 𝑞 <s 𝑦) |
97 | 96 | r19.21bi 3135 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑞 <s 𝑦) |
98 | 82, 84, 85, 87, 97 | slttrd 33958 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑟 <s 𝑦) |
99 | 98 | ralrimiva 3110 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑦 ∈ 𝐵 𝑟 <s 𝑦) |
100 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑟 → (𝑥 <s 𝑦 ↔ 𝑟 <s 𝑦)) |
101 | 100 | ralbidv 3123 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑟 → (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑟 <s 𝑦)) |
102 | 71, 101 | ralsn 4623 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
{𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑟 <s 𝑦) |
103 | 99, 102 | sylibr 233 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
104 | 54, 81, 103 | 3jca 1127 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ({𝑟} ⊆ No
∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) |
105 | | brsslt 33976 |
. . . . . . 7
⊢ ({𝑟} <<s 𝐵 ↔ (({𝑟} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑟} ⊆ No
∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))) |
106 | 80, 104, 105 | sylanbrc 583 |
. . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → {𝑟} <<s 𝐵) |
107 | 48, 78, 106 | jca32 516 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))) |
108 | 107 | exp44 438 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No
∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ))
→ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
109 | 108 | ralrimivvva 3118 |
. . 3
⊢ (𝐴 <<s 𝐵 → ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
110 | | sneq 4577 |
. . . . . . 7
⊢ (𝑦 = 𝑝 → {𝑦} = {𝑝}) |
111 | 110 | breq2d 5091 |
. . . . . 6
⊢ (𝑦 = 𝑝 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑝})) |
112 | 110 | breq1d 5089 |
. . . . . 6
⊢ (𝑦 = 𝑝 → ({𝑦} <<s 𝐵 ↔ {𝑝} <<s 𝐵)) |
113 | 111, 112 | anbi12d 631 |
. . . . 5
⊢ (𝑦 = 𝑝 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵))) |
114 | 113 | ralrab 3632 |
. . . 4
⊢
(∀𝑝 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) ↔ ∀𝑝 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
115 | | sneq 4577 |
. . . . . . . . 9
⊢ (𝑦 = 𝑞 → {𝑦} = {𝑞}) |
116 | 115 | breq2d 5091 |
. . . . . . . 8
⊢ (𝑦 = 𝑞 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑞})) |
117 | 115 | breq1d 5089 |
. . . . . . . 8
⊢ (𝑦 = 𝑞 → ({𝑦} <<s 𝐵 ↔ {𝑞} <<s 𝐵)) |
118 | 116, 117 | anbi12d 631 |
. . . . . . 7
⊢ (𝑦 = 𝑞 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵))) |
119 | 118 | ralrab 3632 |
. . . . . 6
⊢
(∀𝑞 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))) ↔ ∀𝑞 ∈ No
((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) |
120 | | sneq 4577 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑟 → {𝑦} = {𝑟}) |
121 | 120 | breq2d 5091 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑟 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑟})) |
122 | 120 | breq1d 5089 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑟 → ({𝑦} <<s 𝐵 ↔ {𝑟} <<s 𝐵)) |
123 | 121, 122 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑟 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))) |
124 | 123 | elrab 3626 |
. . . . . . . . 9
⊢ (𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))) |
125 | 124 | imbi2i 336 |
. . . . . . . 8
⊢ (((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) |
126 | 125 | ralbii 3093 |
. . . . . . 7
⊢
(∀𝑟 ∈
No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) |
127 | 126 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑞 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑞 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) |
128 | | r19.21v 3103 |
. . . . . . 7
⊢
(∀𝑟 ∈
No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) ↔ ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) |
129 | 128 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑞 ∈
No ∀𝑟 ∈ No
((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) ↔ ∀𝑞 ∈ No
((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) |
130 | 119, 127,
129 | 3bitr4i 303 |
. . . . 5
⊢
(∀𝑞 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) |
131 | 130 | ralbii 3093 |
. . . 4
⊢
(∀𝑝 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑝 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) |
132 | | r19.21v 3103 |
. . . . . . 7
⊢
(∀𝑟 ∈
No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑟 ∈ No
((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
133 | 132 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑞 ∈
No ∀𝑟 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ∀𝑞 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑟 ∈ No
((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
134 | | r19.21v 3103 |
. . . . . 6
⊢
(∀𝑞 ∈
No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑟 ∈ No
((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
135 | 133, 134 | bitri 274 |
. . . . 5
⊢
(∀𝑞 ∈
No ∀𝑟 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
136 | 135 | ralbii 3093 |
. . . 4
⊢
(∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ∀𝑝 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No
∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
137 | 114, 131,
136 | 3bitr4i 303 |
. . 3
⊢
(∀𝑝 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No
∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))) |
138 | 109, 137 | sylibr 233 |
. 2
⊢ (𝐴 <<s 𝐵 → ∀𝑝 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
139 | | nocvxmin 33969 |
. 2
⊢ (({𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ≠ ∅ ∧ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
∧ ∀𝑝 ∈
{𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No
((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) → ∃!𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
140 | 45, 47, 138, 139 | syl3anc 1370 |
1
⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |