| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssltss1 27833 | . . . . . 6
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆  No
) | 
| 2 |  | ssltex1 27831 | . . . . . 6
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) | 
| 3 | 1, 2 | jca 511 | . . . . 5
⊢ (𝐴 <<s 𝐵 → (𝐴 ⊆  No 
∧ 𝐴 ∈
V)) | 
| 4 |  | ssltss2 27834 | . . . . . 6
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆  No
) | 
| 5 |  | ssltex2 27832 | . . . . . 6
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) | 
| 6 | 4, 5 | jca 511 | . . . . 5
⊢ (𝐴 <<s 𝐵 → (𝐵 ⊆  No 
∧ 𝐵 ∈
V)) | 
| 7 |  | ssltsep 27835 | . . . . 5
⊢ (𝐴 <<s 𝐵 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝑦 <s 𝑧) | 
| 8 | 3, 6, 7 | 3jca 1129 | . . . 4
⊢ (𝐴 <<s 𝐵 → ((𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
(𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝑦 <s 𝑧)) | 
| 9 | 8 | 3ad2ant1 1134 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → ((𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
(𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝑦 <s 𝑧)) | 
| 10 |  | 3simpc 1151 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → (𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂)) | 
| 11 |  | noeta 27788 | . . 3
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝑦 <s 𝑧) ∧ (𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂)) → ∃𝑥 ∈ 
No  (∀𝑦
∈ 𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂)) | 
| 12 | 9, 10, 11 | syl2anc 584 | . 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ 
No  (∀𝑦
∈ 𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂)) | 
| 13 | 2 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐴 ∈ V) | 
| 14 |  | vsnex 5434 | . . . . . . . 8
⊢ {𝑥} ∈ V | 
| 15 | 13, 14 | jctir 520 | . . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → (𝐴 ∈ V ∧ {𝑥} ∈ V)) | 
| 16 | 1 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐴 ⊆ 
No ) | 
| 17 |  | snssi 4808 | . . . . . . . . 9
⊢ (𝑥 ∈ 
No  → {𝑥}
⊆  No ) | 
| 18 | 17 | ad2antrl 728 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → {𝑥} ⊆ 
No ) | 
| 19 |  | simprr1 1222 | . . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥) | 
| 20 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 21 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝑦 <s 𝑧 ↔ 𝑦 <s 𝑥)) | 
| 22 | 20, 21 | ralsn 4681 | . . . . . . . . . 10
⊢
(∀𝑧 ∈
{𝑥}𝑦 <s 𝑧 ↔ 𝑦 <s 𝑥) | 
| 23 | 22 | ralbii 3093 | . . . . . . . . 9
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ {𝑥}𝑦 <s 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥) | 
| 24 | 19, 23 | sylibr 234 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ {𝑥}𝑦 <s 𝑧) | 
| 25 | 16, 18, 24 | 3jca 1129 | . . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → (𝐴 ⊆ 
No  ∧ {𝑥}
⊆  No  ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ {𝑥}𝑦 <s 𝑧)) | 
| 26 |  | brsslt 27830 | . . . . . . 7
⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆  No 
∧ {𝑥} ⊆  No  ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ {𝑥}𝑦 <s 𝑧))) | 
| 27 | 15, 25, 26 | sylanbrc 583 | . . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐴 <<s {𝑥}) | 
| 28 | 5 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐵 ∈ V) | 
| 29 | 28, 14 | jctil 519 | . . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ({𝑥} ∈ V ∧ 𝐵 ∈ V)) | 
| 30 | 4 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐵 ⊆ 
No ) | 
| 31 |  | simprr2 1223 | . . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧) | 
| 32 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 <s 𝑧 ↔ 𝑥 <s 𝑧)) | 
| 33 | 32 | ralbidv 3178 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ 𝐵 𝑦 <s 𝑧 ↔ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧)) | 
| 34 | 20, 33 | ralsn 4681 | . . . . . . . . 9
⊢
(∀𝑦 ∈
{𝑥}∀𝑧 ∈ 𝐵 𝑦 <s 𝑧 ↔ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧) | 
| 35 | 31, 34 | sylibr 234 | . . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ∀𝑦 ∈ {𝑥}∀𝑧 ∈ 𝐵 𝑦 <s 𝑧) | 
| 36 | 18, 30, 35 | 3jca 1129 | . . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ({𝑥} ⊆ 
No  ∧ 𝐵 ⊆
 No  ∧ ∀𝑦 ∈ {𝑥}∀𝑧 ∈ 𝐵 𝑦 <s 𝑧)) | 
| 37 |  | brsslt 27830 | . . . . . . 7
⊢ ({𝑥} <<s 𝐵 ↔ (({𝑥} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑥} ⊆  No 
∧ 𝐵 ⊆  No  ∧ ∀𝑦 ∈ {𝑥}∀𝑧 ∈ 𝐵 𝑦 <s 𝑧))) | 
| 38 | 29, 36, 37 | sylanbrc 583 | . . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → {𝑥} <<s 𝐵) | 
| 39 |  | simprr3 1224 | . . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘𝑥) ⊆ 𝑂) | 
| 40 | 27, 38, 39 | 3jca 1129 | . . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ (𝑥 ∈  No 
∧ (∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂)) | 
| 41 | 40 | expr 456 | . . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) ∧ 𝑥 ∈  No )
→ ((∀𝑦 ∈
𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) | 
| 42 | 41 | reximdva 3168 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On) → (∃𝑥 ∈ 
No  (∀𝑦
∈ 𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂) → ∃𝑥 ∈ 
No  (𝐴 <<s
{𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) | 
| 43 | 42 | 3adant3 1133 | . 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → (∃𝑥 ∈ 
No  (∀𝑦
∈ 𝐴 𝑦 <s 𝑥 ∧ ∀𝑧 ∈ 𝐵 𝑥 <s 𝑧 ∧ ( bday
‘𝑥) ⊆
𝑂) → ∃𝑥 ∈ 
No  (𝐴 <<s
{𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) | 
| 44 | 12, 43 | mpd 15 | 1
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ 
No  (𝐴 <<s
{𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂)) |