Step | Hyp | Ref
| Expression |
1 | | nodenselem6 27060 |
. 2
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β No
) |
2 | | bdayval 27019 |
. . . . 5
β’ ((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)}) β No
β ( bday β(π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})) = dom (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)})) = dom (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})) |
4 | | dmres 5963 |
. . . . 5
β’ dom
(π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)}) = (β© {π β On β£ (π΄βπ) β (π΅βπ)} β© dom π΄) |
5 | | nodenselem5 27059 |
. . . . . . . 8
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β©
{π β On β£ (π΄βπ) β (π΅βπ)} β ( bday
βπ΄)) |
6 | | bdayfo 27048 |
. . . . . . . . . . 11
β’ bday : No βontoβOn |
7 | | fof 6760 |
. . . . . . . . . . 11
β’ ( bday : No βontoβOn β bday
: No βΆOn) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
β’ bday : No
βΆOn |
9 | | 0elon 6375 |
. . . . . . . . . 10
β’ β
β On |
10 | 8, 9 | f0cli 7052 |
. . . . . . . . 9
β’ ( bday βπ΄) β On |
11 | 10 | onelssi 6436 |
. . . . . . . 8
β’ (β© {π
β On β£ (π΄βπ) β (π΅βπ)} β ( bday
βπ΄) β
β© {π β On β£ (π΄βπ) β (π΅βπ)} β ( bday
βπ΄)) |
12 | 5, 11 | syl 17 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β©
{π β On β£ (π΄βπ) β (π΅βπ)} β ( bday
βπ΄)) |
13 | | bdayval 27019 |
. . . . . . . 8
β’ (π΄ β
No β ( bday βπ΄) = dom π΄) |
14 | 13 | ad2antrr 725 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ( bday
βπ΄) = dom
π΄) |
15 | 12, 14 | sseqtrd 3988 |
. . . . . 6
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β©
{π β On β£ (π΄βπ) β (π΅βπ)} β dom π΄) |
16 | | df-ss 3931 |
. . . . . 6
β’ (β© {π
β On β£ (π΄βπ) β (π΅βπ)} β dom π΄ β (β© {π β On β£ (π΄βπ) β (π΅βπ)} β© dom π΄) = β© {π β On β£ (π΄βπ) β (π΅βπ)}) |
17 | 15, 16 | sylib 217 |
. . . . 5
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (β©
{π β On β£ (π΄βπ) β (π΅βπ)} β© dom π΄) = β© {π β On β£ (π΄βπ) β (π΅βπ)}) |
18 | 4, 17 | eqtrid 2785 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β dom (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) = β© {π β On β£ (π΄βπ) β (π΅βπ)}) |
19 | 3, 18 | eqtrd 2773 |
. . 3
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)})) = β© {π β On β£ (π΄βπ) β (π΅βπ)}) |
20 | 19, 5 | eqeltrd 2834 |
. 2
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)})) β ( bday
βπ΄)) |
21 | | nodenselem4 27058 |
. . . . 5
β’ (((π΄ β
No β§ π΅ β
No ) β§ π΄ <s π΅) β β© {π β On β£ (π΄βπ) β (π΅βπ)} β On) |
22 | 21 | adantrl 715 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β©
{π β On β£ (π΄βπ) β (π΅βπ)} β On) |
23 | | nodenselem8 27062 |
. . . . . . . . . . . . 13
β’ ((π΄ β
No β§ π΅ β
No β§ ( bday
βπ΄) = ( bday βπ΅)) β (π΄ <s π΅ β ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 2o))) |
24 | 23 | biimpd 228 |
. . . . . . . . . . . 12
β’ ((π΄ β
No β§ π΅ β
No β§ ( bday
βπ΄) = ( bday βπ΅)) β (π΄ <s π΅ β ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 2o))) |
25 | 24 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π΄ β
No β§ π΅ β
No ) β (( bday
βπ΄) = ( bday βπ΅) β (π΄ <s π΅ β ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 2o)))) |
26 | 25 | imp32 420 |
. . . . . . . . . 10
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 2o)) |
27 | 26 | simpld 496 |
. . . . . . . . 9
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o) |
28 | | eqid 2733 |
. . . . . . . . 9
β’ β
=
β
|
29 | 27, 28 | jctir 522 |
. . . . . . . 8
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ β
=
β
)) |
30 | 29 | 3mix1d 1337 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ β
= β
)
β¨ ((π΄ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ β
=
2o) β¨ ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = β
β§ β
=
2o))) |
31 | | fvex 6859 |
. . . . . . . 8
β’ (π΄ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) β V |
32 | | 0ex 5268 |
. . . . . . . 8
β’ β
β V |
33 | 31, 32 | brtp 5484 |
. . . . . . 7
β’ ((π΄ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
,
2oβ©}β
β (((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ β
= β
)
β¨ ((π΄ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 1o β§ β
=
2o) β¨ ((π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = β
β§ β
=
2o))) |
34 | 30, 33 | sylibr 233 |
. . . . . 6
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
,
2oβ©}β
) |
35 | 19 | fveq2d 6850 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})β( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)}))) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)})) |
36 | | fvnobday 27049 |
. . . . . . . 8
β’ ((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)}) β No
β ((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})β( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)}))) = β
) |
37 | 1, 36 | syl 17 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})β( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)}))) = β
) |
38 | 35, 37 | eqtr3d 2775 |
. . . . . 6
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = β
) |
39 | 34, 38 | breqtrrd 5137 |
. . . . 5
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)})) |
40 | | fvres 6865 |
. . . . . . 7
β’ (π¦ β β© {π
β On β£ (π΄βπ) β (π΅βπ)} β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΄βπ¦)) |
41 | 40 | eqcomd 2739 |
. . . . . 6
β’ (π¦ β β© {π
β On β£ (π΄βπ) β (π΅βπ)} β (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦)) |
42 | 41 | rgen 3063 |
. . . . 5
β’
βπ¦ β
β© {π β On β£ (π΄βπ) β (π΅βπ)} (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) |
43 | 39, 42 | jctil 521 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (βπ¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}))) |
44 | | raleq 3308 |
. . . . . 6
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β (βπ¦ β π₯ (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β βπ¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦))) |
45 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β (π΄βπ₯) = (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)})) |
46 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)})) |
47 | 45, 46 | breq12d 5122 |
. . . . . 6
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β ((π΄βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})βπ₯) β (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}))) |
48 | 44, 47 | anbi12d 632 |
. . . . 5
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β ((βπ¦ β π₯ (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})βπ₯)) β (βπ¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)})))) |
49 | 48 | rspcev 3583 |
. . . 4
β’ ((β© {π
β On β£ (π΄βπ) β (π΅βπ)} β On β§ (βπ¦ β β© {π
β On β£ (π΄βπ) β (π΅βπ)} (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}))) β βπ₯ β On (βπ¦ β π₯ (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})βπ₯))) |
50 | 22, 43, 49 | syl2anc 585 |
. . 3
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β βπ₯ β On (βπ¦ β π₯ (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})βπ₯))) |
51 | | simpll 766 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β π΄ β No
) |
52 | | sltval 27018 |
. . . 4
β’ ((π΄ β
No β§ (π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)}) β No )
β (π΄ <s (π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)}) β βπ₯ β On (βπ¦ β π₯ (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})βπ₯)))) |
53 | 51, 1, 52 | syl2anc 585 |
. . 3
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ <s (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β βπ₯ β On (βπ¦ β π₯ (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) β§ (π΄βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)})βπ₯)))) |
54 | 50, 53 | mpbird 257 |
. 2
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β π΄ <s (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})) |
55 | 41 | adantl 483 |
. . . . . 6
β’ ((((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β§ π¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)}) β (π΄βπ¦) = ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦)) |
56 | | nodenselem7 27061 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} β (π΄βπ¦) = (π΅βπ¦))) |
57 | 56 | imp 408 |
. . . . . 6
β’ ((((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β§ π¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)}) β (π΄βπ¦) = (π΅βπ¦)) |
58 | 55, 57 | eqtr3d 2775 |
. . . . 5
β’ ((((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β§ π¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)}) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦)) |
59 | 58 | ralrimiva 3140 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β βπ¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦)) |
60 | 26 | simprd 497 |
. . . . . . . 8
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) = 2o) |
61 | 60, 28 | jctil 521 |
. . . . . . 7
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (β
= β
β§ (π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 2o)) |
62 | 61 | 3mix3d 1339 |
. . . . . 6
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((β
= 1o β§
(π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = β
) β¨ (β
= 1o
β§ (π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 2o) β¨ (β
= β
β§ (π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 2o))) |
63 | | fvex 6859 |
. . . . . . 7
β’ (π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) β V |
64 | 32, 63 | brtp 5484 |
. . . . . 6
β’
(β
{β¨1o, β
β©, β¨1o,
2oβ©, β¨β
, 2oβ©} (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)}) β ((β
= 1o β§
(π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = β
) β¨ (β
= 1o
β§ (π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 2o) β¨ (β
= β
β§ (π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}) = 2o))) |
65 | 62, 64 | sylibr 233 |
. . . . 5
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β β
{β¨1o,
β
β©, β¨1o, 2oβ©, β¨β
,
2oβ©} (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)})) |
66 | 38, 65 | eqbrtrd 5131 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)})) |
67 | | raleq 3308 |
. . . . . 6
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β (βπ¦ β π₯ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β βπ¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦))) |
68 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β (π΅βπ₯) = (π΅ββ© {π β On β£ (π΄βπ) β (π΅βπ)})) |
69 | 46, 68 | breq12d 5122 |
. . . . . 6
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β (((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅βπ₯) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}))) |
70 | 67, 69 | anbi12d 632 |
. . . . 5
β’ (π₯ = β©
{π β On β£ (π΄βπ) β (π΅βπ)} β ((βπ¦ β π₯ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅βπ₯)) β (βπ¦ β β© {π β On β£ (π΄βπ) β (π΅βπ)} ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)})))) |
71 | 70 | rspcev 3583 |
. . . 4
β’ ((β© {π
β On β£ (π΄βπ) β (π΅βπ)} β On β§ (βπ¦ β β© {π
β On β£ (π΄βπ) β (π΅βπ)} ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})ββ© {π β On β£ (π΄βπ) β (π΅βπ)}){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅ββ© {π
β On β£ (π΄βπ) β (π΅βπ)}))) β βπ₯ β On (βπ¦ β π₯ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅βπ₯))) |
72 | 22, 59, 66, 71 | syl12anc 836 |
. . 3
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β βπ₯ β On (βπ¦ β π₯ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅βπ₯))) |
73 | | simplr 768 |
. . . 4
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β π΅ β No
) |
74 | | sltval 27018 |
. . . 4
β’ (((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)}) β No
β§ π΅ β No ) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) <s π΅ β βπ₯ β On (βπ¦ β π₯ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅βπ₯)))) |
75 | 1, 73, 74 | syl2anc 585 |
. . 3
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) <s π΅ β βπ₯ β On (βπ¦ β π₯ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ¦) = (π΅βπ¦) β§ ((π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})βπ₯){β¨1o, β
β©,
β¨1o, 2oβ©, β¨β
, 2oβ©}
(π΅βπ₯)))) |
76 | 72, 75 | mpbird 257 |
. 2
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) <s π΅) |
77 | | fveq2 6846 |
. . . . 5
β’ (π₯ = (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β ( bday
βπ₯) = ( bday β(π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}))) |
78 | 77 | eleq1d 2819 |
. . . 4
β’ (π₯ = (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β (( bday
βπ₯) β
( bday βπ΄) β ( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)})) β ( bday
βπ΄))) |
79 | | breq2 5113 |
. . . 4
β’ (π₯ = (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β (π΄ <s π₯ β π΄ <s (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}))) |
80 | | breq1 5112 |
. . . 4
β’ (π₯ = (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β (π₯ <s π΅ β (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) <s π΅)) |
81 | 78, 79, 80 | 3anbi123d 1437 |
. . 3
β’ (π₯ = (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β ((( bday
βπ₯) β
( bday βπ΄) β§ π΄ <s π₯ β§ π₯ <s π΅) β (( bday
β(π΄ βΎ
β© {π β On β£ (π΄βπ) β (π΅βπ)})) β ( bday
βπ΄) β§
π΄ <s (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β§ (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) <s π΅))) |
82 | 81 | rspcev 3583 |
. 2
β’ (((π΄ βΎ β© {π
β On β£ (π΄βπ) β (π΅βπ)}) β No
β§ (( bday β(π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)})) β ( bday
βπ΄) β§
π΄ <s (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) β§ (π΄ βΎ β© {π β On β£ (π΄βπ) β (π΅βπ)}) <s π΅)) β βπ₯ β No
(( bday βπ₯) β ( bday
βπ΄) β§
π΄ <s π₯ β§ π₯ <s π΅)) |
83 | 1, 20, 54, 76, 82 | syl13anc 1373 |
1
β’ (((π΄ β
No β§ π΅ β
No ) β§ (( bday
βπ΄) = ( bday βπ΅) β§ π΄ <s π΅)) β βπ₯ β No
(( bday βπ₯) β ( bday
βπ΄) β§
π΄ <s π₯ β§ π₯ <s π΅)) |