Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐴 <<s 𝐵) |
2 | | scutcut 33992 |
. . . . . . 7
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
4 | 3 | simp2d 1142 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐴 <<s {(𝐴 |s 𝐵)}) |
5 | | simp2 1136 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐶 <<s {(𝐴 |s 𝐵)}) |
6 | | ssltun1 33999 |
. . . . 5
⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝐶 <<s {(𝐴 |s 𝐵)}) → (𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)}) |
7 | 4, 5, 6 | syl2anc 584 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)}) |
8 | 3 | simp3d 1143 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → {(𝐴 |s 𝐵)} <<s 𝐵) |
9 | | simp3 1137 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → {(𝐴 |s 𝐵)} <<s 𝐷) |
10 | | ssltun2 34000 |
. . . . 5
⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷)) |
11 | 8, 9, 10 | syl2anc 584 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷)) |
12 | | ovex 7310 |
. . . . . 6
⊢ (𝐴 |s 𝐵) ∈ V |
13 | 12 | snnz 4714 |
. . . . 5
⊢ {(𝐴 |s 𝐵)} ≠ ∅ |
14 | | sslttr 33998 |
. . . . 5
⊢ (((𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷) ∧ {(𝐴 |s 𝐵)} ≠ ∅) → (𝐴 ∪ 𝐶) <<s (𝐵 ∪ 𝐷)) |
15 | 13, 14 | mp3an3 1449 |
. . . 4
⊢ (((𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷)) → (𝐴 ∪ 𝐶) <<s (𝐵 ∪ 𝐷)) |
16 | 7, 11, 15 | syl2anc 584 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (𝐴 ∪ 𝐶) <<s (𝐵 ∪ 𝐷)) |
17 | | scutval 33991 |
. . 3
⊢ ((𝐴 ∪ 𝐶) <<s (𝐵 ∪ 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (℩𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}))) |
18 | 16, 17 | syl 17 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (℩𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}))) |
19 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
20 | 19 | elima 5976 |
. . . . . . . . 9
⊢ (𝑥 ∈ (
bday “ {𝑦
∈ No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ↔ ∃𝑧 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}𝑧 bday 𝑥) |
21 | | sneq 4573 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
22 | 21 | breq2d 5088 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝐴 ∪ 𝐶) <<s {𝑦} ↔ (𝐴 ∪ 𝐶) <<s {𝑧})) |
23 | 21 | breq1d 5086 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ({𝑦} <<s (𝐵 ∪ 𝐷) ↔ {𝑧} <<s (𝐵 ∪ 𝐷))) |
24 | 22, 23 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷)) ↔ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷)))) |
25 | 24 | rexrab 3634 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
{𝑦 ∈ No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}𝑧 bday 𝑥 ↔ ∃𝑧 ∈
No (((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷)) ∧ 𝑧 bday 𝑥)) |
26 | 20, 25 | bitri 274 |
. . . . . . . 8
⊢ (𝑥 ∈ (
bday “ {𝑦
∈ No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ↔ ∃𝑧 ∈ No
(((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷)) ∧ 𝑧 bday 𝑥)) |
27 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → 𝑧 ∈ No
) |
28 | | bdayfn 33965 |
. . . . . . . . . . . . . 14
⊢ bday Fn No
|
29 | | fnbrfvb 6824 |
. . . . . . . . . . . . . 14
⊢ (( bday Fn No ∧ 𝑧 ∈
No ) → (( bday ‘𝑧) = 𝑥 ↔ 𝑧 bday 𝑥)) |
30 | 28, 29 | mpan 687 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
No → (( bday ‘𝑧) = 𝑥 ↔ 𝑧 bday 𝑥)) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → (( bday
‘𝑧) = 𝑥 ↔ 𝑧 bday 𝑥)) |
32 | | simpll1 1211 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → 𝐴 <<s 𝐵) |
33 | | scutbday 33995 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
35 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → (𝐴 ∪ 𝐶) <<s {𝑧}) |
36 | | ssun1 4107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐶) |
37 | | sssslt1 33986 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∪ 𝐶) <<s {𝑧} ∧ 𝐴 ⊆ (𝐴 ∪ 𝐶)) → 𝐴 <<s {𝑧}) |
38 | 36, 37 | mpan2 688 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∪ 𝐶) <<s {𝑧} → 𝐴 <<s {𝑧}) |
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → 𝐴 <<s {𝑧}) |
40 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → {𝑧} <<s (𝐵 ∪ 𝐷)) |
41 | | ssun1 4107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 ⊆ (𝐵 ∪ 𝐷) |
42 | | sssslt2 33987 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝑧} <<s (𝐵 ∪ 𝐷) ∧ 𝐵 ⊆ (𝐵 ∪ 𝐷)) → {𝑧} <<s 𝐵) |
43 | 41, 42 | mpan2 688 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑧} <<s (𝐵 ∪ 𝐷) → {𝑧} <<s 𝐵) |
44 | 40, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → {𝑧} <<s 𝐵) |
45 | 39, 44 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)) |
46 | 21 | breq2d 5088 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑧})) |
47 | 21 | breq1d 5086 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → ({𝑦} <<s 𝐵 ↔ {𝑧} <<s 𝐵)) |
48 | 46, 47 | anbi12d 631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))) |
49 | 48 | elrab 3625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑧 ∈ No
∧ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))) |
50 | 27, 45, 49 | sylanbrc 583 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → 𝑧 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
51 | | ssrab2 4014 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
|
52 | | fnfvima 7111 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday Fn No ∧ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
∧ 𝑧 ∈ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday
‘𝑧) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
53 | 28, 51, 52 | mp3an12 1450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} → ( bday
‘𝑧) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
54 | 50, 53 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → ( bday
‘𝑧) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
55 | | intss1 4896 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑧) ∈ ( bday
“ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑧)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑧)) |
57 | 34, 56 | eqsstrd 3960 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧)) |
58 | | sseq2 3948 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑧) = 𝑥 → (( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧) ↔ ( bday
‘(𝐴 |s 𝐵)) ⊆ 𝑥)) |
59 | 58 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝑧) = 𝑥 → (( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧) → ( bday
‘(𝐴 |s 𝐵)) ⊆ 𝑥)) |
60 | 59 | com12 32 |
. . . . . . . . . . . . 13
⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday
‘𝑧) →
(( bday ‘𝑧) = 𝑥 → ( bday
‘(𝐴 |s 𝐵)) ⊆ 𝑥)) |
61 | 57, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → (( bday
‘𝑧) = 𝑥 → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑥)) |
62 | 31, 61 | sylbird 259 |
. . . . . . . . . . 11
⊢ ((((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
∧ ((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷))) → (𝑧 bday 𝑥 → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑥)) |
63 | 62 | ex 413 |
. . . . . . . . . 10
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
→ (((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷)) → (𝑧 bday 𝑥 → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑥))) |
64 | 63 | impd 411 |
. . . . . . . . 9
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) ∧ 𝑧 ∈ No )
→ ((((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷)) ∧ 𝑧 bday 𝑥) → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑥)) |
65 | 64 | rexlimdva 3212 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (∃𝑧 ∈ No
(((𝐴 ∪ 𝐶) <<s {𝑧} ∧ {𝑧} <<s (𝐵 ∪ 𝐷)) ∧ 𝑧 bday 𝑥) → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑥)) |
66 | 26, 65 | syl5bi 241 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (𝑥 ∈ ( bday
“ {𝑦 ∈ No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) → ( bday
‘(𝐴 |s 𝐵)) ⊆ 𝑥)) |
67 | 66 | ralrimiv 3102 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ∀𝑥 ∈ ( bday
“ {𝑦 ∈ No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})( bday
‘(𝐴 |s 𝐵)) ⊆ 𝑥) |
68 | | ssint 4897 |
. . . . . 6
⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ∩
( bday “ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ↔ ∀𝑥 ∈ ( bday
“ {𝑦 ∈ No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})( bday
‘(𝐴 |s 𝐵)) ⊆ 𝑥) |
69 | 67, 68 | sylibr 233 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
70 | 3 | simp1d 1141 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (𝐴 |s 𝐵) ∈ No
) |
71 | 7, 11 | jca 512 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷))) |
72 | | sneq 4573 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 |s 𝐵) → {𝑦} = {(𝐴 |s 𝐵)}) |
73 | 72 | breq2d 5088 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 |s 𝐵) → ((𝐴 ∪ 𝐶) <<s {𝑦} ↔ (𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)})) |
74 | 72 | breq1d 5086 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 |s 𝐵) → ({𝑦} <<s (𝐵 ∪ 𝐷) ↔ {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷))) |
75 | 73, 74 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 |s 𝐵) → (((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷)) ↔ ((𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷)))) |
76 | 75 | elrab 3625 |
. . . . . . . 8
⊢ ((𝐴 |s 𝐵) ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ↔ ((𝐴 |s 𝐵) ∈ No
∧ ((𝐴 ∪ 𝐶) <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s (𝐵 ∪ 𝐷)))) |
77 | 70, 71, 76 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (𝐴 |s 𝐵) ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) |
78 | | ssrab2 4014 |
. . . . . . . 8
⊢ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ⊆ No
|
79 | | fnfvima 7111 |
. . . . . . . 8
⊢ (( bday Fn No ∧ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ⊆ No
∧ (𝐴 |s 𝐵) ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) → ( bday
‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
80 | 28, 78, 79 | mp3an12 1450 |
. . . . . . 7
⊢ ((𝐴 |s 𝐵) ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} → ( bday
‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
81 | 77, 80 | syl 17 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ( bday
‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
82 | | intss1 4896 |
. . . . . 6
⊢ (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday
“ {𝑦 ∈
No ∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) → ∩
( bday “ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ⊆ ( bday
‘(𝐴 |s 𝐵))) |
83 | 81, 82 | syl 17 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ∩ ( bday “ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ⊆ ( bday
‘(𝐴 |s 𝐵))) |
84 | 69, 83 | eqssd 3939 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
85 | | conway 33990 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐶) <<s (𝐵 ∪ 𝐷) → ∃!𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
86 | 16, 85 | syl 17 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ∃!𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) |
87 | | fveqeq2 6785 |
. . . . . 6
⊢ (𝑥 = (𝐴 |s 𝐵) → (( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ↔ ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}))) |
88 | 87 | riota2 7260 |
. . . . 5
⊢ (((𝐴 |s 𝐵) ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ∧ ∃!𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) → (( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ↔ (℩𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) = (𝐴 |s 𝐵))) |
89 | 77, 86, 88 | syl2anc 584 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}) ↔ (℩𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) = (𝐴 |s 𝐵))) |
90 | 84, 89 | mpbid 231 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (℩𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))})) = (𝐴 |s 𝐵)) |
91 | 90 | eqcomd 2744 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No
∣ ((𝐴 ∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ ((𝐴
∪ 𝐶) <<s {𝑦} ∧ {𝑦} <<s (𝐵 ∪ 𝐷))}))) |
92 | 18, 91 | eqtr4d 2781 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵)) |