| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssltss1 |
⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No ) |
| 2 |
|
ssltex1 |
⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V ) |
| 3 |
1 2
|
jca |
⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ) |
| 4 |
|
ssltss2 |
⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No ) |
| 5 |
|
ssltex2 |
⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V ) |
| 6 |
4 5
|
jca |
⊢ ( 𝐴 <<s 𝐵 → ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) |
| 7 |
|
ssltsep |
⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) |
| 8 |
3 6 7
|
3jca |
⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) ) |
| 9 |
8
|
3ad2ant1 |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) ) |
| 10 |
|
3simpc |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) |
| 11 |
|
noeta |
⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ∃ 𝑥 ∈ No ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) |
| 12 |
9 10 11
|
syl2anc |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ∃ 𝑥 ∈ No ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) |
| 13 |
2
|
ad2antrr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 ∈ V ) |
| 14 |
|
snex |
⊢ { 𝑥 } ∈ V |
| 15 |
13 14
|
jctir |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( 𝐴 ∈ V ∧ { 𝑥 } ∈ V ) ) |
| 16 |
1
|
ad2antrr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 ⊆ No ) |
| 17 |
|
snssi |
⊢ ( 𝑥 ∈ No → { 𝑥 } ⊆ No ) |
| 18 |
17
|
ad2antrl |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → { 𝑥 } ⊆ No ) |
| 19 |
|
simprr1 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ) |
| 20 |
|
vex |
⊢ 𝑥 ∈ V |
| 21 |
|
breq2 |
⊢ ( 𝑧 = 𝑥 → ( 𝑦 <s 𝑧 ↔ 𝑦 <s 𝑥 ) ) |
| 22 |
20 21
|
ralsn |
⊢ ( ∀ 𝑧 ∈ { 𝑥 } 𝑦 <s 𝑧 ↔ 𝑦 <s 𝑥 ) |
| 23 |
22
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 } 𝑦 <s 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ) |
| 24 |
19 23
|
sylibr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 } 𝑦 <s 𝑧 ) |
| 25 |
16 18 24
|
3jca |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( 𝐴 ⊆ No ∧ { 𝑥 } ⊆ No ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 } 𝑦 <s 𝑧 ) ) |
| 26 |
|
brsslt |
⊢ ( 𝐴 <<s { 𝑥 } ↔ ( ( 𝐴 ∈ V ∧ { 𝑥 } ∈ V ) ∧ ( 𝐴 ⊆ No ∧ { 𝑥 } ⊆ No ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 } 𝑦 <s 𝑧 ) ) ) |
| 27 |
15 25 26
|
sylanbrc |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s { 𝑥 } ) |
| 28 |
5
|
ad2antrr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐵 ∈ V ) |
| 29 |
28 14
|
jctil |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( { 𝑥 } ∈ V ∧ 𝐵 ∈ V ) ) |
| 30 |
4
|
ad2antrr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐵 ⊆ No ) |
| 31 |
|
simprr2 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ) |
| 32 |
|
breq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 <s 𝑧 ↔ 𝑥 <s 𝑧 ) ) |
| 33 |
32
|
ralbidv |
⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ↔ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ) ) |
| 34 |
20 33
|
ralsn |
⊢ ( ∀ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ↔ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ) |
| 35 |
31 34
|
sylibr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ∀ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) |
| 36 |
18 30 35
|
3jca |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( { 𝑥 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) ) |
| 37 |
|
brsslt |
⊢ ( { 𝑥 } <<s 𝐵 ↔ ( ( { 𝑥 } ∈ V ∧ 𝐵 ∈ V ) ∧ ( { 𝑥 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝐵 𝑦 <s 𝑧 ) ) ) |
| 38 |
29 36 37
|
sylanbrc |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → { 𝑥 } <<s 𝐵 ) |
| 39 |
|
simprr3 |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ 𝑥 ) ⊆ 𝑂 ) |
| 40 |
27 38 39
|
3jca |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ ( 𝑥 ∈ No ∧ ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) |
| 41 |
40
|
expr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) ∧ 𝑥 ∈ No ) → ( ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) |
| 42 |
41
|
reximdva |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ) → ( ∃ 𝑥 ∈ No ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) |
| 43 |
42
|
3adant3 |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ( ∃ 𝑥 ∈ No ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) |
| 44 |
12 43
|
mpd |
⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) |