Step | Hyp | Ref
| Expression |
1 | | simplr 528 |
. . . . . . . . . . 11
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β πΊ:πβ1-1βπ« 1o) |
2 | | f1f 5421 |
. . . . . . . . . . 11
β’ (πΊ:πβ1-1βπ« 1o β πΊ:πβΆπ«
1o) |
3 | 1, 2 | syl 14 |
. . . . . . . . . 10
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β πΊ:πβΆπ«
1o) |
4 | | nnon 4609 |
. . . . . . . . . . . . . 14
β’ (π β Ο β π β On) |
5 | 4 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β π β On) |
6 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
2o β π) |
7 | | 1lt2o 6442 |
. . . . . . . . . . . . . 14
β’
1o β 2o |
8 | 6, 7 | jctil 312 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
(1o β 2o β§ 2o β π)) |
9 | | ontr1 4389 |
. . . . . . . . . . . . 13
β’ (π β On β
((1o β 2o β§ 2o β π) β 1o β
π)) |
10 | 5, 8, 9 | sylc 62 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
1o β π) |
11 | | 0lt1o 6440 |
. . . . . . . . . . . 12
β’ β
β 1o |
12 | | opelxpi 4658 |
. . . . . . . . . . . 12
β’
((1o β π β§ β
β 1o) β
β¨1o, β
β© β (π Γ 1o)) |
13 | 10, 11, 12 | sylancl 413 |
. . . . . . . . . . 11
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
β¨1o, β
β© β (π Γ 1o)) |
14 | | pwle2.t |
. . . . . . . . . . . 12
β’ π = βͺ π₯ β π ({π₯} Γ 1o) |
15 | | iunxpconst 4686 |
. . . . . . . . . . . 12
β’ βͺ π₯ β π ({π₯} Γ 1o) = (π Γ 1o) |
16 | 14, 15 | eqtri 2198 |
. . . . . . . . . . 11
β’ π = (π Γ 1o) |
17 | 13, 16 | eleqtrrdi 2271 |
. . . . . . . . . 10
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
β¨1o, β
β© β π) |
18 | 3, 17 | ffvelcdmd 5652 |
. . . . . . . . 9
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨1o,
β
β©) β π« 1o) |
19 | 18 | elpwid 3586 |
. . . . . . . 8
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨1o,
β
β©) β 1o) |
20 | | df1o2 6429 |
. . . . . . . 8
β’
1o = {β
} |
21 | 19, 20 | sseqtrdi 3203 |
. . . . . . 7
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨1o,
β
β©) β {β
}) |
22 | | pwtrufal 14717 |
. . . . . . 7
β’ ((πΊββ¨1o,
β
β©) β {β
} β Β¬ Β¬ ((πΊββ¨1o, β
β©) =
β
β¨ (πΊββ¨1o, β
β©) =
{β
})) |
23 | 21, 22 | syl 14 |
. . . . . 6
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
Β¬ ((πΊββ¨1o, β
β©) =
β
β¨ (πΊββ¨1o, β
β©) =
{β
})) |
24 | | ioran 752 |
. . . . . 6
β’ (Β¬
((πΊββ¨1o, β
β©) =
β
β¨ (πΊββ¨1o, β
β©) =
{β
}) β (Β¬ (πΊββ¨1o, β
β©) =
β
β§ Β¬ (πΊββ¨1o, β
β©) =
{β
})) |
25 | 23, 24 | sylnib 676 |
. . . . 5
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(Β¬ (πΊββ¨1o, β
β©) =
β
β§ Β¬ (πΊββ¨1o, β
β©) =
{β
})) |
26 | | 1n0 6432 |
. . . . . . . . . . 11
β’
1o β β
|
27 | 26 | neii 2349 |
. . . . . . . . . 10
β’ Β¬
1o = β
|
28 | | 1oex 6424 |
. . . . . . . . . . 11
β’
1o β V |
29 | | 0ex 4130 |
. . . . . . . . . . 11
β’ β
β V |
30 | 28, 29 | opth1 4236 |
. . . . . . . . . 10
β’
(β¨1o, β
β© = β¨β
, β
β©
β 1o = β
) |
31 | 27, 30 | mto 662 |
. . . . . . . . 9
β’ Β¬
β¨1o, β
β© = β¨β
,
β
β© |
32 | | 0lt2o 6441 |
. . . . . . . . . . . . . 14
β’ β
β 2o |
33 | 6, 32 | jctil 312 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (β
β 2o β§ 2o β π)) |
34 | | ontr1 4389 |
. . . . . . . . . . . . 13
β’ (π β On β ((β
β 2o β§ 2o β π) β β
β π)) |
35 | 5, 33, 34 | sylc 62 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β β
β π) |
36 | | opelxpi 4658 |
. . . . . . . . . . . 12
β’ ((β
β π β§ β
β 1o) β β¨β
, β
β© β (π Γ
1o)) |
37 | 35, 11, 36 | sylancl 413 |
. . . . . . . . . . 11
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
β¨β
, β
β© β (π Γ 1o)) |
38 | 37, 16 | eleqtrrdi 2271 |
. . . . . . . . . 10
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
β¨β
, β
β© β π) |
39 | | f1veqaeq 5769 |
. . . . . . . . . 10
β’ ((πΊ:πβ1-1βπ« 1o β§
(β¨1o, β
β© β π β§ β¨β
, β
β© β
π)) β ((πΊββ¨1o,
β
β©) = (πΊββ¨β
, β
β©) β
β¨1o, β
β© = β¨β
,
β
β©)) |
40 | 1, 17, 38, 39 | syl12anc 1236 |
. . . . . . . . 9
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β ((πΊββ¨1o,
β
β©) = (πΊββ¨β
, β
β©) β
β¨1o, β
β© = β¨β
,
β
β©)) |
41 | 31, 40 | mtoi 664 |
. . . . . . . 8
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(πΊββ¨1o, β
β©) =
(πΊββ¨β
,
β
β©)) |
42 | 41 | adantr 276 |
. . . . . . 7
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β Β¬ (πΊββ¨1o, β
β©) =
(πΊββ¨β
,
β
β©)) |
43 | | simpr 110 |
. . . . . . . 8
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β (πΊββ¨β
, β
β©) =
β
) |
44 | 43 | eqeq2d 2189 |
. . . . . . 7
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β ((πΊββ¨1o, β
β©) =
(πΊββ¨β
,
β
β©) β (πΊββ¨1o, β
β©) =
β
)) |
45 | 42, 44 | mtbid 672 |
. . . . . 6
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β Β¬ (πΊββ¨1o, β
β©) =
β
) |
46 | | 2on0 6426 |
. . . . . . . . . . . . . 14
β’
2o β β
|
47 | 46 | nesymi 2393 |
. . . . . . . . . . . . 13
β’ Β¬
β
= 2o |
48 | 29, 29 | opth1 4236 |
. . . . . . . . . . . . 13
β’
(β¨β
, β
β© = β¨2o, β
β©
β β
= 2o) |
49 | 47, 48 | mto 662 |
. . . . . . . . . . . 12
β’ Β¬
β¨β
, β
β© = β¨2o,
β
β© |
50 | | opelxpi 4658 |
. . . . . . . . . . . . . . 15
β’
((2o β π β§ β
β 1o) β
β¨2o, β
β© β (π Γ 1o)) |
51 | 6, 11, 50 | sylancl 413 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
β¨2o, β
β© β (π Γ 1o)) |
52 | 51, 16 | eleqtrrdi 2271 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β
β¨2o, β
β© β π) |
53 | | f1veqaeq 5769 |
. . . . . . . . . . . . 13
β’ ((πΊ:πβ1-1βπ« 1o β§ (β¨β
,
β
β© β π
β§ β¨2o, β
β© β π)) β ((πΊββ¨β
, β
β©) =
(πΊββ¨2o, β
β©)
β β¨β
, β
β© = β¨2o,
β
β©)) |
54 | 1, 38, 52, 53 | syl12anc 1236 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β ((πΊββ¨β
,
β
β©) = (πΊββ¨2o, β
β©)
β β¨β
, β
β© = β¨2o,
β
β©)) |
55 | 49, 54 | mtoi 664 |
. . . . . . . . . . 11
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(πΊββ¨β
,
β
β©) = (πΊββ¨2o,
β
β©)) |
56 | 55 | ad2antrr 488 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ (πΊββ¨β
, β
β©) =
(πΊββ¨2o,
β
β©)) |
57 | | simplr 528 |
. . . . . . . . . . 11
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β (πΊββ¨β
, β
β©) =
β
) |
58 | 57 | eqeq1d 2186 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β ((πΊββ¨β
, β
β©) =
(πΊββ¨2o, β
β©)
β β
= (πΊββ¨2o,
β
β©))) |
59 | 56, 58 | mtbid 672 |
. . . . . . . . 9
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ β
= (πΊββ¨2o,
β
β©)) |
60 | | eqcom 2179 |
. . . . . . . . 9
β’ (β
= (πΊββ¨2o, β
β©)
β (πΊββ¨2o, β
β©) =
β
) |
61 | 59, 60 | sylnib 676 |
. . . . . . . 8
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ (πΊββ¨2o, β
β©) =
β
) |
62 | | 1onn 6520 |
. . . . . . . . . . . . . . . . . 18
β’
1o β Ο |
63 | | peano1 4593 |
. . . . . . . . . . . . . . . . . 18
β’ β
β Ο |
64 | | peano4 4596 |
. . . . . . . . . . . . . . . . . 18
β’
((1o β Ο β§ β
β Ο) β (suc
1o = suc β
β 1o = β
)) |
65 | 62, 63, 64 | mp2an 426 |
. . . . . . . . . . . . . . . . 17
β’ (suc
1o = suc β
β 1o = β
) |
66 | 26, 65 | nemtbir 2436 |
. . . . . . . . . . . . . . . 16
β’ Β¬
suc 1o = suc β
|
67 | | df-2o 6417 |
. . . . . . . . . . . . . . . . 17
β’
2o = suc 1o |
68 | | df-1o 6416 |
. . . . . . . . . . . . . . . . 17
β’
1o = suc β
|
69 | 67, 68 | eqeq12i 2191 |
. . . . . . . . . . . . . . . 16
β’
(2o = 1o β suc 1o = suc
β
) |
70 | 66, 69 | mtbir 671 |
. . . . . . . . . . . . . . 15
β’ Β¬
2o = 1o |
71 | 70 | neir 2350 |
. . . . . . . . . . . . . 14
β’
2o β 1o |
72 | 71 | nesymi 2393 |
. . . . . . . . . . . . 13
β’ Β¬
1o = 2o |
73 | 28, 29 | opth1 4236 |
. . . . . . . . . . . . 13
β’
(β¨1o, β
β© = β¨2o, β
β©
β 1o = 2o) |
74 | 72, 73 | mto 662 |
. . . . . . . . . . . 12
β’ Β¬
β¨1o, β
β© = β¨2o,
β
β© |
75 | | f1veqaeq 5769 |
. . . . . . . . . . . . 13
β’ ((πΊ:πβ1-1βπ« 1o β§
(β¨1o, β
β© β π β§ β¨2o, β
β©
β π)) β ((πΊββ¨1o,
β
β©) = (πΊββ¨2o, β
β©)
β β¨1o, β
β© = β¨2o,
β
β©)) |
76 | 1, 17, 52, 75 | syl12anc 1236 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β ((πΊββ¨1o,
β
β©) = (πΊββ¨2o, β
β©)
β β¨1o, β
β© = β¨2o,
β
β©)) |
77 | 74, 76 | mtoi 664 |
. . . . . . . . . . 11
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(πΊββ¨1o, β
β©) =
(πΊββ¨2o,
β
β©)) |
78 | 77 | ad2antrr 488 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ (πΊββ¨1o, β
β©) =
(πΊββ¨2o,
β
β©)) |
79 | | simpr 110 |
. . . . . . . . . . 11
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β (πΊββ¨1o, β
β©) =
{β
}) |
80 | 79 | eqeq1d 2186 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β ((πΊββ¨1o, β
β©) =
(πΊββ¨2o, β
β©)
β {β
} = (πΊββ¨2o,
β
β©))) |
81 | 78, 80 | mtbid 672 |
. . . . . . . . 9
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ {β
} = (πΊββ¨2o,
β
β©)) |
82 | | eqcom 2179 |
. . . . . . . . 9
β’
({β
} = (πΊββ¨2o, β
β©)
β (πΊββ¨2o, β
β©) =
{β
}) |
83 | 81, 82 | sylnib 676 |
. . . . . . . 8
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ (πΊββ¨2o, β
β©) =
{β
}) |
84 | 61, 83 | jca 306 |
. . . . . . 7
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β (Β¬ (πΊββ¨2o, β
β©) =
β
β§ Β¬ (πΊββ¨2o, β
β©) =
{β
})) |
85 | 3, 52 | ffvelcdmd 5652 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨2o,
β
β©) β π« 1o) |
86 | 85 | elpwid 3586 |
. . . . . . . . . . 11
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨2o,
β
β©) β 1o) |
87 | 86, 20 | sseqtrdi 3203 |
. . . . . . . . . 10
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨2o,
β
β©) β {β
}) |
88 | | pwtrufal 14717 |
. . . . . . . . . 10
β’ ((πΊββ¨2o,
β
β©) β {β
} β Β¬ Β¬ ((πΊββ¨2o, β
β©) =
β
β¨ (πΊββ¨2o, β
β©) =
{β
})) |
89 | 87, 88 | syl 14 |
. . . . . . . . 9
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
Β¬ ((πΊββ¨2o, β
β©) =
β
β¨ (πΊββ¨2o, β
β©) =
{β
})) |
90 | | ioran 752 |
. . . . . . . . 9
β’ (Β¬
((πΊββ¨2o, β
β©) =
β
β¨ (πΊββ¨2o, β
β©) =
{β
}) β (Β¬ (πΊββ¨2o, β
β©) =
β
β§ Β¬ (πΊββ¨2o, β
β©) =
{β
})) |
91 | 89, 90 | sylnib 676 |
. . . . . . . 8
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(Β¬ (πΊββ¨2o, β
β©) =
β
β§ Β¬ (πΊββ¨2o, β
β©) =
{β
})) |
92 | 91 | ad2antrr 488 |
. . . . . . 7
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β§ (πΊββ¨1o, β
β©) =
{β
}) β Β¬ (Β¬ (πΊββ¨2o, β
β©) =
β
β§ Β¬ (πΊββ¨2o, β
β©) =
{β
})) |
93 | 84, 92 | pm2.65da 661 |
. . . . . 6
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β Β¬ (πΊββ¨1o, β
β©) =
{β
}) |
94 | 45, 93 | jca 306 |
. . . . 5
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = β
) β (Β¬ (πΊββ¨1o, β
β©) =
β
β§ Β¬ (πΊββ¨1o, β
β©) =
{β
})) |
95 | 25, 94 | mtand 665 |
. . . 4
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(πΊββ¨β
,
β
β©) = β
) |
96 | | eqcom 2179 |
. . . . . . . . . . 11
β’ ((πΊββ¨1o,
β
β©) = (πΊββ¨2o, β
β©)
β (πΊββ¨2o, β
β©) =
(πΊββ¨1o,
β
β©)) |
97 | 77, 96 | sylnib 676 |
. . . . . . . . . 10
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(πΊββ¨2o, β
β©) =
(πΊββ¨1o,
β
β©)) |
98 | 97 | ad2antrr 488 |
. . . . . . . . 9
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β Β¬ (πΊββ¨2o, β
β©) =
(πΊββ¨1o,
β
β©)) |
99 | | simpr 110 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β (πΊββ¨1o, β
β©) =
β
) |
100 | 99 | eqeq2d 2189 |
. . . . . . . . 9
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β ((πΊββ¨2o, β
β©) =
(πΊββ¨1o, β
β©)
β (πΊββ¨2o, β
β©) =
β
)) |
101 | 98, 100 | mtbid 672 |
. . . . . . . 8
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β Β¬ (πΊββ¨2o, β
β©) =
β
) |
102 | 55 | ad2antrr 488 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β Β¬ (πΊββ¨β
, β
β©) =
(πΊββ¨2o,
β
β©)) |
103 | | eqcom 2179 |
. . . . . . . . . 10
β’ ((πΊββ¨β
,
β
β©) = (πΊββ¨2o, β
β©)
β (πΊββ¨2o, β
β©) =
(πΊββ¨β
,
β
β©)) |
104 | 102, 103 | sylnib 676 |
. . . . . . . . 9
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β Β¬ (πΊββ¨2o, β
β©) =
(πΊββ¨β
,
β
β©)) |
105 | | simplr 528 |
. . . . . . . . . 10
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β (πΊββ¨β
, β
β©) =
{β
}) |
106 | 105 | eqeq2d 2189 |
. . . . . . . . 9
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β ((πΊββ¨2o, β
β©) =
(πΊββ¨β
,
β
β©) β (πΊββ¨2o, β
β©) =
{β
})) |
107 | 104, 106 | mtbid 672 |
. . . . . . . 8
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β Β¬ (πΊββ¨2o, β
β©) =
{β
}) |
108 | 101, 107 | jca 306 |
. . . . . . 7
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β (Β¬ (πΊββ¨2o, β
β©) =
β
β§ Β¬ (πΊββ¨2o, β
β©) =
{β
})) |
109 | 91 | ad2antrr 488 |
. . . . . . 7
β’
(((((π β
Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β§ (πΊββ¨1o, β
β©) =
β
) β Β¬ (Β¬ (πΊββ¨2o, β
β©) =
β
β§ Β¬ (πΊββ¨2o, β
β©) =
{β
})) |
110 | 108, 109 | pm2.65da 661 |
. . . . . 6
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β Β¬ (πΊββ¨1o, β
β©) =
β
) |
111 | 41 | adantr 276 |
. . . . . . 7
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β Β¬ (πΊββ¨1o, β
β©) =
(πΊββ¨β
,
β
β©)) |
112 | | simpr 110 |
. . . . . . . 8
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β (πΊββ¨β
, β
β©) =
{β
}) |
113 | 112 | eqeq2d 2189 |
. . . . . . 7
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β ((πΊββ¨1o, β
β©) =
(πΊββ¨β
,
β
β©) β (πΊββ¨1o, β
β©) =
{β
})) |
114 | 111, 113 | mtbid 672 |
. . . . . 6
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β Β¬ (πΊββ¨1o, β
β©) =
{β
}) |
115 | 110, 114 | jca 306 |
. . . . 5
β’ ((((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β§ (πΊββ¨β
,
β
β©) = {β
}) β (Β¬ (πΊββ¨1o, β
β©) =
β
β§ Β¬ (πΊββ¨1o, β
β©) =
{β
})) |
116 | 25, 115 | mtand 665 |
. . . 4
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(πΊββ¨β
,
β
β©) = {β
}) |
117 | 95, 116 | jca 306 |
. . 3
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (Β¬
(πΊββ¨β
,
β
β©) = β
β§ Β¬ (πΊββ¨β
, β
β©) =
{β
})) |
118 | 3, 38 | ffvelcdmd 5652 |
. . . . . . 7
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨β
,
β
β©) β π« 1o) |
119 | 118 | elpwid 3586 |
. . . . . 6
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨β
,
β
β©) β 1o) |
120 | 119, 20 | sseqtrdi 3203 |
. . . . 5
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β (πΊββ¨β
,
β
β©) β {β
}) |
121 | | pwtrufal 14717 |
. . . . 5
β’ ((πΊββ¨β
,
β
β©) β {β
} β Β¬ Β¬ ((πΊββ¨β
, β
β©) =
β
β¨ (πΊββ¨β
, β
β©) =
{β
})) |
122 | 120, 121 | syl 14 |
. . . 4
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
Β¬ ((πΊββ¨β
, β
β©) =
β
β¨ (πΊββ¨β
, β
β©) =
{β
})) |
123 | | ioran 752 |
. . . 4
β’ (Β¬
((πΊββ¨β
,
β
β©) = β
β¨ (πΊββ¨β
, β
β©) =
{β
}) β (Β¬ (πΊββ¨β
, β
β©) =
β
β§ Β¬ (πΊββ¨β
, β
β©) =
{β
})) |
124 | 122, 123 | sylnib 676 |
. . 3
β’ (((π β Ο β§ πΊ:πβ1-1βπ« 1o) β§ 2o
β π) β Β¬
(Β¬ (πΊββ¨β
, β
β©) =
β
β§ Β¬ (πΊββ¨β
, β
β©) =
{β
})) |
125 | 117, 124 | pm2.65da 661 |
. 2
β’ ((π β Ο β§ πΊ:πβ1-1βπ« 1o) β Β¬
2o β π) |
126 | | 2onn 6521 |
. . . 4
β’
2o β Ο |
127 | | nntri1 6496 |
. . . 4
β’ ((π β Ο β§
2o β Ο) β (π β 2o β Β¬
2o β π)) |
128 | 126, 127 | mpan2 425 |
. . 3
β’ (π β Ο β (π β 2o β
Β¬ 2o β π)) |
129 | 128 | adantr 276 |
. 2
β’ ((π β Ο β§ πΊ:πβ1-1βπ« 1o) β (π β 2o β
Β¬ 2o β π)) |
130 | 125, 129 | mpbird 167 |
1
β’ ((π β Ο β§ πΊ:πβ1-1βπ« 1o) β π β
2o) |