Step | Hyp | Ref
| Expression |
1 | | nfv 1528 |
. . . . . . . 8
β’
β²π π β (π«
1o Γ Ο) |
2 | | nfv 1528 |
. . . . . . . . 9
β’
β²πβπ β π« 1oβπ β Ο πππ |
3 | | nfre1 2520 |
. . . . . . . . 9
β’
β²πβπ β Ο βπ β π«
1oπππ |
4 | 2, 3 | nfim 1572 |
. . . . . . . 8
β’
β²π(βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ) |
5 | 1, 4 | nfim 1572 |
. . . . . . 7
β’
β²π(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) |
6 | 5 | nfal 1576 |
. . . . . 6
β’
β²πβπ(π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) |
7 | | nfv 1528 |
. . . . . 6
β’
β²π π:Οβontoβπ« 1o |
8 | 6, 7 | nfan 1565 |
. . . . 5
β’
β²π(βπ(π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) |
9 | | breq1 4006 |
. . . . . . . . 9
β’ (π = β
β (πβ‘ππ β β
β‘ππ)) |
10 | | simpr 110 |
. . . . . . . . 9
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β βπ β π« 1oπβ‘ππ) |
11 | | 0elpw 4164 |
. . . . . . . . . 10
β’ β
β π« 1o |
12 | 11 | a1i 9 |
. . . . . . . . 9
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β β
β π«
1o) |
13 | 9, 10, 12 | rspcdva 2846 |
. . . . . . . 8
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β β
β‘ππ) |
14 | | 0ex 4130 |
. . . . . . . . 9
β’ β
β V |
15 | | vex 2740 |
. . . . . . . . 9
β’ π β V |
16 | 14, 15 | brcnv 4810 |
. . . . . . . 8
β’
(β
β‘ππ β ππβ
) |
17 | 13, 16 | sylib 122 |
. . . . . . 7
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β ππβ
) |
18 | | fofn 5440 |
. . . . . . . . 9
β’ (π:Οβontoβπ« 1o β π Fn Ο) |
19 | 18 | ad3antlr 493 |
. . . . . . . 8
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β π Fn Ο) |
20 | | simplr 528 |
. . . . . . . 8
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β π β Ο) |
21 | | fnbrfvb 5556 |
. . . . . . . 8
β’ ((π Fn Ο β§ π β Ο) β ((πβπ) = β
β ππβ
)) |
22 | 19, 20, 21 | syl2anc 411 |
. . . . . . 7
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β ((πβπ) = β
β ππβ
)) |
23 | 17, 22 | mpbird 167 |
. . . . . 6
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β (πβπ) = β
) |
24 | | breq1 4006 |
. . . . . . . . . 10
β’ (π = 1o β (πβ‘ππ β 1oβ‘ππ)) |
25 | | 1oex 6424 |
. . . . . . . . . . . 12
β’
1o β V |
26 | 25 | pwid 3590 |
. . . . . . . . . . 11
β’
1o β π« 1o |
27 | 26 | a1i 9 |
. . . . . . . . . 10
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β 1o β π«
1o) |
28 | 24, 10, 27 | rspcdva 2846 |
. . . . . . . . 9
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β 1oβ‘ππ) |
29 | 25, 15 | brcnv 4810 |
. . . . . . . . 9
β’
(1oβ‘ππ β ππ1o) |
30 | 28, 29 | sylib 122 |
. . . . . . . 8
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β ππ1o) |
31 | | fnbrfvb 5556 |
. . . . . . . . 9
β’ ((π Fn Ο β§ π β Ο) β ((πβπ) = 1o β ππ1o)) |
32 | 19, 20, 31 | syl2anc 411 |
. . . . . . . 8
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β ((πβπ) = 1o β ππ1o)) |
33 | 30, 32 | mpbird 167 |
. . . . . . 7
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β (πβπ) = 1o) |
34 | | 1n0 6432 |
. . . . . . . 8
β’
1o β β
|
35 | 34 | neii 2349 |
. . . . . . 7
β’ Β¬
1o = β
|
36 | | eqeq1 2184 |
. . . . . . . . 9
β’ ((πβπ) = 1o β ((πβπ) = β
β 1o =
β
)) |
37 | 36 | biimpd 144 |
. . . . . . . 8
β’ ((πβπ) = 1o β ((πβπ) = β
β 1o =
β
)) |
38 | 37 | con3dimp 635 |
. . . . . . 7
β’ (((πβπ) = 1o β§ Β¬ 1o =
β
) β Β¬ (πβπ) = β
) |
39 | 33, 35, 38 | sylancl 413 |
. . . . . 6
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β Β¬ (πβπ) = β
) |
40 | 23, 39 | pm2.21fal 1373 |
. . . . 5
β’
((((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β§ π β Ο) β§
βπ β π«
1oπβ‘ππ) β β₯) |
41 | | fof 5438 |
. . . . . . . 8
β’ (π:Οβontoβπ« 1o β π:ΟβΆπ«
1o) |
42 | | fssxp 5383 |
. . . . . . . . . 10
β’ (π:ΟβΆπ«
1o β π
β (Ο Γ π« 1o)) |
43 | | cnvss 4800 |
. . . . . . . . . 10
β’ (π β (Ο Γ
π« 1o) β β‘π β β‘(Ο Γ π«
1o)) |
44 | 42, 43 | syl 14 |
. . . . . . . . 9
β’ (π:ΟβΆπ«
1o β β‘π β β‘(Ο Γ π«
1o)) |
45 | | cnvxp 5047 |
. . . . . . . . 9
β’ β‘(Ο Γ π« 1o) =
(π« 1o Γ Ο) |
46 | 44, 45 | sseqtrdi 3203 |
. . . . . . . 8
β’ (π:ΟβΆπ«
1o β β‘π β (π«
1o Γ Ο)) |
47 | 41, 46 | syl 14 |
. . . . . . 7
β’ (π:Οβontoβπ« 1o β β‘π β (π« 1o Γ
Ο)) |
48 | 47 | adantl 277 |
. . . . . 6
β’
((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β β‘π β (π« 1o Γ
Ο)) |
49 | | foelrn 5753 |
. . . . . . . . 9
β’ ((π:Οβontoβπ« 1o β§ π β π« 1o)
β βπ β
Ο π = (πβπ)) |
50 | 18 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π:Οβontoβπ« 1o β§ π β π« 1o)
β§ π β Ο)
β π Fn
Ο) |
51 | | simpr 110 |
. . . . . . . . . . 11
β’ (((π:Οβontoβπ« 1o β§ π β π« 1o)
β§ π β Ο)
β π β
Ο) |
52 | | eqcom 2179 |
. . . . . . . . . . . 12
β’ ((πβπ) = π β π = (πβπ)) |
53 | | fnbrfvb 5556 |
. . . . . . . . . . . . 13
β’ ((π Fn Ο β§ π β Ο) β ((πβπ) = π β πππ)) |
54 | | brcnvg 4808 |
. . . . . . . . . . . . . . 15
β’ ((π β V β§ π β V) β (πβ‘ππ β πππ)) |
55 | 54 | elvd 2742 |
. . . . . . . . . . . . . 14
β’ (π β V β (πβ‘ππ β πππ)) |
56 | 55 | elv 2741 |
. . . . . . . . . . . . 13
β’ (πβ‘ππ β πππ) |
57 | 53, 56 | bitr4di 198 |
. . . . . . . . . . . 12
β’ ((π Fn Ο β§ π β Ο) β ((πβπ) = π β πβ‘ππ)) |
58 | 52, 57 | bitr3id 194 |
. . . . . . . . . . 11
β’ ((π Fn Ο β§ π β Ο) β (π = (πβπ) β πβ‘ππ)) |
59 | 50, 51, 58 | syl2anc 411 |
. . . . . . . . . 10
β’ (((π:Οβontoβπ« 1o β§ π β π« 1o)
β§ π β Ο)
β (π = (πβπ) β πβ‘ππ)) |
60 | 59 | rexbidva 2474 |
. . . . . . . . 9
β’ ((π:Οβontoβπ« 1o β§ π β π« 1o)
β (βπ β
Ο π = (πβπ) β βπ β Ο πβ‘ππ)) |
61 | 49, 60 | mpbid 147 |
. . . . . . . 8
β’ ((π:Οβontoβπ« 1o β§ π β π« 1o)
β βπ β
Ο πβ‘ππ) |
62 | 61 | ralrimiva 2550 |
. . . . . . 7
β’ (π:Οβontoβπ« 1o β βπ β π«
1oβπ
β Ο πβ‘ππ) |
63 | 62 | adantl 277 |
. . . . . 6
β’
((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β βπ β π«
1oβπ
β Ο πβ‘ππ) |
64 | | cnvexg 5166 |
. . . . . . . 8
β’ (π β V β β‘π β V) |
65 | 64 | elv 2741 |
. . . . . . 7
β’ β‘π β V |
66 | | simpl 109 |
. . . . . . 7
β’
((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β βπ(π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ))) |
67 | | sseq1 3178 |
. . . . . . . . 9
β’ (π = β‘π β (π β (π« 1o Γ
Ο) β β‘π β (π« 1o Γ
Ο))) |
68 | | breq 4005 |
. . . . . . . . . . . 12
β’ (π = β‘π β (πππ β πβ‘ππ)) |
69 | 68 | rexbidv 2478 |
. . . . . . . . . . 11
β’ (π = β‘π β (βπ β Ο πππ β βπ β Ο πβ‘ππ)) |
70 | 69 | ralbidv 2477 |
. . . . . . . . . 10
β’ (π = β‘π β (βπ β π« 1oβπ β Ο πππ β βπ β π« 1oβπ β Ο πβ‘ππ)) |
71 | | breq 4005 |
. . . . . . . . . . . 12
β’ (π = β‘π β (πππ β πβ‘ππ)) |
72 | 71 | ralbidv 2477 |
. . . . . . . . . . 11
β’ (π = β‘π β (βπ β π« 1oπππ β βπ β π« 1oπβ‘ππ)) |
73 | 72 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π = β‘π β (βπ β Ο βπ β π« 1oπππ β βπ β Ο βπ β π« 1oπβ‘ππ)) |
74 | 70, 73 | imbi12d 234 |
. . . . . . . . 9
β’ (π = β‘π β ((βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ) β (βπ β π« 1oβπ β Ο πβ‘ππ β βπ β Ο βπ β π« 1oπβ‘ππ))) |
75 | 67, 74 | imbi12d 234 |
. . . . . . . 8
β’ (π = β‘π β ((π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β (β‘π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πβ‘ππ β βπ β Ο βπ β π« 1oπβ‘ππ)))) |
76 | 75 | spcgv 2824 |
. . . . . . 7
β’ (β‘π β V β (βπ(π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β (β‘π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πβ‘ππ β βπ β Ο βπ β π« 1oπβ‘ππ)))) |
77 | 65, 66, 76 | mpsyl 65 |
. . . . . 6
β’
((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β (β‘π β (π« 1o Γ
Ο) β (βπ
β π« 1oβπ β Ο πβ‘ππ β βπ β Ο βπ β π« 1oπβ‘ππ))) |
78 | 48, 63, 77 | mp2d 47 |
. . . . 5
β’
((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β βπ β Ο βπ β π«
1oπβ‘ππ) |
79 | 8, 40, 78 | r19.29af 2618 |
. . . 4
β’
((βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β§ π:Οβontoβπ« 1o) β
β₯) |
80 | 79 | inegd 1372 |
. . 3
β’
(βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β Β¬ π:Οβontoβπ« 1o) |
81 | 80 | nexdv 1936 |
. 2
β’
(βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β Β¬ βπ π:Οβontoβπ« 1o) |
82 | | elex2 2753 |
. . 3
β’ (β
β π« 1o β βπ€ π€ β π«
1o) |
83 | | ctm 7107 |
. . 3
β’
(βπ€ π€ β π« 1o
β (βπ π:Οβontoβ(π« 1o β
1o) β βπ π:Οβontoβπ« 1o)) |
84 | 11, 82, 83 | mp2b 8 |
. 2
β’
(βπ π:Οβontoβ(π« 1o β
1o) β βπ π:Οβontoβπ« 1o) |
85 | 81, 84 | sylnibr 677 |
1
β’
(βπ(π β (π«
1o Γ Ο) β (βπ β π« 1oβπ β Ο πππ β βπ β Ο βπ β π« 1oπππ)) β Β¬ βπ π:Οβontoβ(π« 1o β
1o)) |