Step | Hyp | Ref
| Expression |
1 | | fodjuomnilemdc.fo |
. . . . . 6
β’ (π β πΉ:πβontoβ(π΄ β π΅)) |
2 | | fof 5450 |
. . . . . 6
β’ (πΉ:πβontoβ(π΄ β π΅) β πΉ:πβΆ(π΄ β π΅)) |
3 | 1, 2 | syl 14 |
. . . . 5
β’ (π β πΉ:πβΆ(π΄ β π΅)) |
4 | 3 | ffvelcdmda 5664 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β (π΄ β π΅)) |
5 | | djur 7081 |
. . . 4
β’ ((πΉβπ) β (π΄ β π΅) β (βπ§ β π΄ (πΉβπ) = (inlβπ§) β¨ βπ§ β π΅ (πΉβπ) = (inrβπ§))) |
6 | 4, 5 | sylib 122 |
. . 3
β’ ((π β§ π β π) β (βπ§ β π΄ (πΉβπ) = (inlβπ§) β¨ βπ§ β π΅ (πΉβπ) = (inrβπ§))) |
7 | | nfv 1538 |
. . . . . . . 8
β’
β²π§(π β§ π β π) |
8 | | nfre1 2530 |
. . . . . . . 8
β’
β²π§βπ§ β π΅ (πΉβπ) = (inrβπ§) |
9 | 7, 8 | nfan 1575 |
. . . . . . 7
β’
β²π§((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) |
10 | | simpr 110 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β βπ§ β π΅ (πΉβπ) = (inrβπ§)) |
11 | | fveq2 5527 |
. . . . . . . . . . . 12
β’ (π§ = π€ β (inrβπ§) = (inrβπ€)) |
12 | 11 | eqeq2d 2199 |
. . . . . . . . . . 11
β’ (π§ = π€ β ((πΉβπ) = (inrβπ§) β (πΉβπ) = (inrβπ€))) |
13 | 12 | cbvrexv 2716 |
. . . . . . . . . 10
β’
(βπ§ β
π΅ (πΉβπ) = (inrβπ§) β βπ€ β π΅ (πΉβπ) = (inrβπ€)) |
14 | 10, 13 | sylib 122 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β βπ€ β π΅ (πΉβπ) = (inrβπ€)) |
15 | | vex 2752 |
. . . . . . . . . . . . . . 15
β’ π§ β V |
16 | | vex 2752 |
. . . . . . . . . . . . . . 15
β’ π€ β V |
17 | | djune 7090 |
. . . . . . . . . . . . . . 15
β’ ((π§ β V β§ π€ β V) β
(inlβπ§) β
(inrβπ€)) |
18 | 15, 16, 17 | mp2an 426 |
. . . . . . . . . . . . . 14
β’
(inlβπ§) β
(inrβπ€) |
19 | | neeq2 2371 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) = (inrβπ€) β ((inlβπ§) β (πΉβπ) β (inlβπ§) β (inrβπ€))) |
20 | 18, 19 | mpbiri 168 |
. . . . . . . . . . . . 13
β’ ((πΉβπ) = (inrβπ€) β (inlβπ§) β (πΉβπ)) |
21 | 20 | necomd 2443 |
. . . . . . . . . . . 12
β’ ((πΉβπ) = (inrβπ€) β (πΉβπ) β (inlβπ§)) |
22 | 21 | neneqd 2378 |
. . . . . . . . . . 11
β’ ((πΉβπ) = (inrβπ€) β Β¬ (πΉβπ) = (inlβπ§)) |
23 | 22 | a1i 9 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β ((πΉβπ) = (inrβπ€) β Β¬ (πΉβπ) = (inlβπ§))) |
24 | 23 | rexlimdvw 2608 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β (βπ€ β π΅ (πΉβπ) = (inrβπ€) β Β¬ (πΉβπ) = (inlβπ§))) |
25 | 14, 24 | mpd 13 |
. . . . . . . 8
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β Β¬ (πΉβπ) = (inlβπ§)) |
26 | 25 | a1d 22 |
. . . . . . 7
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β (π§ β π΄ β Β¬ (πΉβπ) = (inlβπ§))) |
27 | 9, 26 | ralrimi 2558 |
. . . . . 6
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β βπ§ β π΄ Β¬ (πΉβπ) = (inlβπ§)) |
28 | | ralnex 2475 |
. . . . . 6
β’
(βπ§ β
π΄ Β¬ (πΉβπ) = (inlβπ§) β Β¬ βπ§ β π΄ (πΉβπ) = (inlβπ§)) |
29 | 27, 28 | sylib 122 |
. . . . 5
β’ (((π β§ π β π) β§ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β Β¬ βπ§ β π΄ (πΉβπ) = (inlβπ§)) |
30 | 29 | ex 115 |
. . . 4
β’ ((π β§ π β π) β (βπ§ β π΅ (πΉβπ) = (inrβπ§) β Β¬ βπ§ β π΄ (πΉβπ) = (inlβπ§))) |
31 | 30 | orim2d 789 |
. . 3
β’ ((π β§ π β π) β ((βπ§ β π΄ (πΉβπ) = (inlβπ§) β¨ βπ§ β π΅ (πΉβπ) = (inrβπ§)) β (βπ§ β π΄ (πΉβπ) = (inlβπ§) β¨ Β¬ βπ§ β π΄ (πΉβπ) = (inlβπ§)))) |
32 | 6, 31 | mpd 13 |
. 2
β’ ((π β§ π β π) β (βπ§ β π΄ (πΉβπ) = (inlβπ§) β¨ Β¬ βπ§ β π΄ (πΉβπ) = (inlβπ§))) |
33 | | df-dc 836 |
. 2
β’
(DECID βπ§ β π΄ (πΉβπ) = (inlβπ§) β (βπ§ β π΄ (πΉβπ) = (inlβπ§) β¨ Β¬ βπ§ β π΄ (πΉβπ) = (inlβπ§))) |
34 | 32, 33 | sylibr 134 |
1
β’ ((π β§ π β π) β DECID βπ§ β π΄ (πΉβπ) = (inlβπ§)) |