Step | Hyp | Ref
| Expression |
1 | | eusn 4691 |
. . . 4
β’
(β!π π β (π΄π»π·) β βπ(π΄π»π·) = {π}) |
2 | | initoeu2lem.x |
. . . . . . . . . . . 12
β’ π = (BaseβπΆ) |
3 | | eqid 2736 |
. . . . . . . . . . . 12
β’
(InvβπΆ) =
(InvβπΆ) |
4 | | initoeu1.c |
. . . . . . . . . . . . 13
β’ (π β πΆ β Cat) |
5 | 4 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β πΆ β Cat) |
6 | | simpr2 1195 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β π΅ β π) |
7 | 6 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β π΅ β π) |
8 | | simpr1 1194 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β π΄ β π) |
9 | 8 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β π΄ β π) |
10 | | initoeu2lem.i |
. . . . . . . . . . . 12
β’ πΌ = (IsoβπΆ) |
11 | 2, 3, 5, 7, 9, 10 | invf 17651 |
. . . . . . . . . . 11
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β (π΅(InvβπΆ)π΄):(π΅πΌπ΄)βΆ(π΄πΌπ΅)) |
12 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β πΎ β (π΅πΌπ΄)) |
13 | 11, 12 | ffvelcdmd 7036 |
. . . . . . . . . 10
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) |
14 | | initoeu2lem.h |
. . . . . . . . . . . . . . . . . 18
β’ π» = (Hom βπΆ) |
15 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β πΆ β Cat) |
16 | 2, 14, 10, 15, 8, 6 | isohom 17659 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β (π΄πΌπ΅) β (π΄π»π΅)) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β (π΄πΌπ΅) β (π΄π»π΅)) |
18 | 17 | sselda 3944 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) |
19 | | initoeu2lem.o |
. . . . . . . . . . . . . . . . . 18
β’ β¬ =
(compβπΆ) |
20 | 15 | ad4antr 730 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β πΆ β Cat) |
21 | 8 | ad4antr 730 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β π΄ β π) |
22 | 6 | ad4antr 730 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β π΅ β π) |
23 | | simpr3 1196 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β π· β π) |
24 | 23 | ad4antr 730 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β π· β π) |
25 | | simplr 767 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) |
26 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β πΊ β (π΅π»π·)) |
27 | 2, 14, 19, 20, 21, 22, 24, 25, 26 | catcocl 17565 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·)) |
28 | 15 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β πΆ β Cat) |
29 | 8 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β π΄ β π) |
30 | 6 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β π΅ β π) |
31 | 23 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β π· β π) |
32 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) |
33 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) |
34 | 2, 14, 19, 28, 29, 30, 31, 32, 33 | catcocl 17565 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·)) |
35 | 34 | exp31 420 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β (((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·)))) |
36 | 35 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β (((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·)))) |
37 | 36 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·))) |
38 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π΄π»π·) = {π} β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π})) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π})) |
40 | | ovex 7390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β V |
41 | | elsng 4600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β V β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
42 | 40, 41 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
43 | 39, 42 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
44 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π΄π»π·) = {π} β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π})) |
45 | | ovex 7390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β V |
46 | | elsng 4600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β V β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π} β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
47 | 45, 46 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π΄π»π·) = {π} β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β {π} β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
48 | 44, 47 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π΄π»π·) = {π} β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π)) |
50 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)))) |
51 | 50 | eqcoms 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)))) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)))) |
53 | | simp-4l 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β§ (πΊ β (π΅π»π·) β§ πΉ β (π΄π»π·))) β (π β§ (π΄ β π β§ π΅ β π β§ π· β π))) |
54 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β§ (πΊ β (π΅π»π·) β§ πΉ β (π΄π»π·))) β πΎ β (π΅πΌπ΄)) |
55 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β§ (πΊ β (π΅π»π·) β§ πΉ β (π΄π»π·))) β πΉ β (π΄π»π·)) |
56 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β§ (πΊ β (π΅π»π·) β§ πΉ β (π΄π»π·))) β πΊ β (π΅π»π·)) |
57 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β§ (πΊ β (π΅π»π·) β§ πΉ β (π΄π»π·))) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) |
58 | | initoeu1.a |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β π΄ β (InitOβπΆ)) |
59 | 4, 58, 2, 14, 10, 19 | initoeu2lem0 17899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)) |
60 | 53, 54, 55, 56, 57, 59 | syl131anc 1383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β§ (πΊ β (π΅π»π·) β§ πΉ β (π΄π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)) |
61 | 60 | exp43 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))) |
63 | 52, 62 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))) |
64 | 63 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
66 | 49, 65 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
67 | 66 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = π β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
68 | 43, 67 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
69 | 68 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ (π΄π»π·) = {π}) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
70 | 69 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β ((π΄π»π·) = {π} β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))))) |
71 | 70 | com24 95 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((π΄π»π·) = {π} β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))))) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β (((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((π΄π»π·) = {π} β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))))) |
73 | 37, 72 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((π΄π»π·) = {π} β (πΊ β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))))) |
74 | 73 | com25 99 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β (πΊ β (π΅π»π·) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))))) |
75 | 74 | imp 407 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β (π΄π»π·) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
76 | 27, 75 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β§ πΊ β (π΅π»π·)) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))) |
77 | 76 | ex 413 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄π»π΅)) β (πΊ β (π΅π»π·) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
78 | 18, 77 | mpdan 685 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β (πΊ β (π΅π»π·) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (πΉ β (π΄π»π·) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
79 | 78 | com15 101 |
. . . . . . . . . . . . 13
β’ (πΉ β (π΄π»π·) β (πΊ β (π΅π»π·) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))))) |
80 | 79 | imp 407 |
. . . . . . . . . . . 12
β’ ((πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β ((π΄π»π·) = {π} β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))))) |
81 | 80 | impcom 408 |
. . . . . . . . . . 11
β’ (((π΄π»π·) = {π} β§ (πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
82 | 81 | com13 88 |
. . . . . . . . . 10
β’ ((((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β§ ((π΅(InvβπΆ)π΄)βπΎ) β (π΄πΌπ΅)) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (((π΄π»π·) = {π} β§ (πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
83 | 13, 82 | mpdan 685 |
. . . . . . . . 9
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ πΎ β (π΅πΌπ΄)) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·) β (((π΄π»π·) = {π} β§ (πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
84 | 83 | expimpd 454 |
. . . . . . . 8
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β ((πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·)) β (((π΄π»π·) = {π} β§ (πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
85 | 84 | 3impia 1117 |
. . . . . . 7
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β (((π΄π»π·) = {π} β§ (πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))) |
86 | 85 | com12 32 |
. . . . . 6
β’ (((π΄π»π·) = {π} β§ (πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))) |
87 | 86 | ex 413 |
. . . . 5
β’ ((π΄π»π·) = {π} β ((πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
88 | 87 | exlimiv 1933 |
. . . 4
β’
(βπ(π΄π»π·) = {π} β ((πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
89 | 1, 88 | sylbi 216 |
. . 3
β’
(β!π π β (π΄π»π·) β ((πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)))) |
90 | 89 | 3impib 1116 |
. 2
β’
((β!π π β (π΄π»π·) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))) |
91 | 90 | com12 32 |
1
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β ((β!π π β (π΄π»π·) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))) |