Step | Hyp | Ref
| Expression |
1 | | simp3l 1202 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s {(𝐴 |s 𝐵)}) |
2 | | simp3r 1203 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {(𝐴 |s 𝐵)} <<s 𝐷) |
3 | | simp1 1137 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 <<s 𝐵) |
4 | | scutbday 33653 |
. . . . . 6
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐴
<<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
6 | | ssltex1 33636 |
. . . . . . . . . . . . 13
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
7 | 3, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ∈ V) |
8 | 7 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ V) |
9 | | ssltss1 33638 |
. . . . . . . . . . . . 13
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
10 | 3, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ⊆ No
) |
11 | 10 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ 𝐶 <<s {𝑡}) → 𝐴 ⊆ No
) |
12 | 8, 11 | elpwd 4506 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ 𝒫 No
) |
13 | | simpl2l 1227 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
→ ∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦) |
14 | 13 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ 𝐶 <<s {𝑡}) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦) |
15 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ 𝐶 <<s {𝑡}) → 𝐶 <<s {𝑡}) |
16 | | cofsslt 33743 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡}) |
17 | 12, 14, 15, 16 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡}) |
18 | 17 | ex 416 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
→ (𝐶 <<s {𝑡} → 𝐴 <<s {𝑡})) |
19 | | ssltex2 33637 |
. . . . . . . . . . . . 13
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
20 | 3, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ∈ V) |
21 | 20 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ {𝑡} <<s 𝐷) → 𝐵 ∈ V) |
22 | | ssltss2 33639 |
. . . . . . . . . . . . 13
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
23 | 3, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ⊆ No
) |
24 | 23 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ {𝑡} <<s 𝐷) → 𝐵 ⊆ No
) |
25 | 21, 24 | elpwd 4506 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ {𝑡} <<s 𝐷) → 𝐵 ∈ 𝒫 No
) |
26 | | simpl2r 1228 |
. . . . . . . . . . 11
⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
→ ∀𝑧 ∈
𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) |
27 | 26 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ {𝑡} <<s 𝐷) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) |
28 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐷) |
29 | | coinitsslt 33744 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵) |
30 | 25, 27, 28, 29 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵) |
31 | 30 | ex 416 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
→ ({𝑡} <<s 𝐷 → {𝑡} <<s 𝐵)) |
32 | 18, 31 | anim12d 612 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No )
→ ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) → (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵))) |
33 | 32 | ss2rabdv 3975 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) |
34 | | imass2 5949 |
. . . . . 6
⊢ ({𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} → ( bday
“ {𝑡 ∈
No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday
“ {𝑡 ∈
No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})) |
35 | | intss 4867 |
. . . . . 6
⊢ (( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday
“ {𝑡 ∈
No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ∩
( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})) |
36 | 33, 34, 35 | 3syl 18 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ∩
( bday “ {𝑡 ∈ No
∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ∩
( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})) |
37 | 5, 36 | eqsstrd 3925 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ∩ ( bday “ {𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)})) |
38 | | bdayfn 33623 |
. . . . . 6
⊢ bday Fn No
|
39 | | ssrab2 3979 |
. . . . . 6
⊢ {𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No
|
40 | | sneq 4536 |
. . . . . . . . 9
⊢ (𝑡 = (𝐴 |s 𝐵) → {𝑡} = {(𝐴 |s 𝐵)}) |
41 | 40 | breq2d 5052 |
. . . . . . . 8
⊢ (𝑡 = (𝐴 |s 𝐵) → (𝐶 <<s {𝑡} ↔ 𝐶 <<s {(𝐴 |s 𝐵)})) |
42 | 40 | breq1d 5050 |
. . . . . . . 8
⊢ (𝑡 = (𝐴 |s 𝐵) → ({𝑡} <<s 𝐷 ↔ {(𝐴 |s 𝐵)} <<s 𝐷)) |
43 | 41, 42 | anbi12d 634 |
. . . . . . 7
⊢ (𝑡 = (𝐴 |s 𝐵) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷))) |
44 | 3 | scutcld 33652 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ No
) |
45 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) |
46 | 43, 44, 45 | elrabd 3595 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) |
47 | | fnfvima 7018 |
. . . . . 6
⊢ (( bday Fn No ∧ {𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No
∧ (𝐴 |s 𝐵) ∈ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ( bday
‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})) |
48 | 38, 39, 46, 47 | mp3an12i 1466 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday
‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})) |
49 | | intss1 4861 |
. . . . 5
⊢ (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday
“ {𝑡 ∈
No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ∩
( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday
‘(𝐴 |s 𝐵))) |
50 | 48, 49 | syl 17 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ∩
( bday “ {𝑡 ∈ No
∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday
‘(𝐴 |s 𝐵))) |
51 | 37, 50 | eqssd 3904 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)})) |
52 | | ovex 7215 |
. . . . . . 7
⊢ (𝐴 |s 𝐵) ∈ V |
53 | 52 | snnz 4677 |
. . . . . 6
⊢ {(𝐴 |s 𝐵)} ≠ ∅ |
54 | | sslttr 33656 |
. . . . . 6
⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ {(𝐴 |s 𝐵)} ≠ ∅) → 𝐶 <<s 𝐷) |
55 | 53, 54 | mp3an3 1451 |
. . . . 5
⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐶 <<s 𝐷) |
56 | 55 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s 𝐷) |
57 | | eqscut 33654 |
. . . 4
⊢ ((𝐶 <<s 𝐷 ∧ (𝐴 |s 𝐵) ∈ No )
→ ((𝐶 |s 𝐷) = (𝐴 |s 𝐵) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)})))) |
58 | 56, 44, 57 | syl2anc 587 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ((𝐶 |s 𝐷) = (𝐴 |s 𝐵) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈
No ∣ (𝐶
<<s {𝑡} ∧ {𝑡} <<s 𝐷)})))) |
59 | 1, 2, 51, 58 | mpbir3and 1343 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 |s 𝐷) = (𝐴 |s 𝐵)) |
60 | 59 | eqcomd 2745 |
1
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) |