Step | Hyp | Ref
| Expression |
1 | | grumnudlem.2 |
. . . . . . . 8
β’ (π β πΊ β Univ) |
2 | | gruss 10791 |
. . . . . . . 8
β’ ((πΊ β Univ β§ π§ β πΊ β§ π β π§) β π β πΊ) |
3 | 1, 2 | syl3an1 1164 |
. . . . . . 7
β’ ((π β§ π§ β πΊ β§ π β π§) β π β πΊ) |
4 | 3 | 3expia 1122 |
. . . . . 6
β’ ((π β§ π§ β πΊ) β (π β π§ β π β πΊ)) |
5 | 4 | alrimiv 1931 |
. . . . 5
β’ ((π β§ π§ β πΊ) β βπ(π β π§ β π β πΊ)) |
6 | | pwss 4626 |
. . . . 5
β’
(π« π§ β
πΊ β βπ(π β π§ β π β πΊ)) |
7 | 5, 6 | sylibr 233 |
. . . 4
β’ ((π β§ π§ β πΊ) β π« π§ β πΊ) |
8 | | ssun1 4173 |
. . . . . . . . 9
β’ π«
π§ β (π« π§ βͺ βͺ (πΉ
Coll π§)) |
9 | | simp3 1139 |
. . . . . . . . 9
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) |
10 | 8, 9 | sseqtrrid 4036 |
. . . . . . . 8
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β π« π§ β π€) |
11 | | simp1l3 1269 |
. . . . . . . . . . 11
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) |
12 | | simp1r 1199 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π β π§) |
13 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β = βͺ
π£ β§ π = π£) β π = π£) |
14 | 13 | unieqd 4923 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β = βͺ
π£ β§ π = π£) β βͺ π = βͺ
π£) |
15 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β = βͺ
π£ β§ π = π£) β β = βͺ π£) |
16 | 14, 15 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β = βͺ
π£ β§ π = π£) β βͺ π = β) |
17 | 16 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β βͺ π = β) |
18 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π = π£) |
19 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β (π β π£ β§ π£ β π)) |
20 | 19 | simprd 497 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π£ β π) |
21 | 18, 20 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π β π) |
22 | 19 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π β π£) |
23 | 22, 18 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π β π) |
24 | 17, 21, 23 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β (βͺ π = β β§ π β π β§ π β π)) |
25 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β π£ β πΊ) |
26 | 24, 25 | rr-spce 42956 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β βπ(βͺ
π = β β§ π β π β§ π β π)) |
27 | | simp1l1 1267 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π) |
28 | 27, 1 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β πΊ β Univ) |
29 | | simp2 1138 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π£ β πΊ) |
30 | | gruuni 10795 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β Univ β§ π£ β πΊ) β βͺ π£ β πΊ) |
31 | 28, 29, 30 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β βͺ π£ β πΊ) |
32 | 26, 31 | rspcime 3617 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β πΊ βπ(βͺ π = β β§ π β π β§ π β π)) |
33 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π) |
34 | 33, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β πΊ β Univ) |
35 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π§ β πΊ) |
36 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π β π§) |
37 | | gruel 10798 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ β Univ β§ π§ β πΊ β§ π β π§) β π β πΊ) |
38 | 34, 35, 36, 37 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π β πΊ) |
39 | 38 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π β πΊ) |
40 | | grumnudlem.4 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β πΊ β§ β β πΊ) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) |
41 | 39, 40 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β πΊ) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) |
42 | 41 | rexbidva 3177 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β (ββ β πΊ ππΉβ β ββ β πΊ βπ(βͺ π = β β§ π β π β§ π β π))) |
43 | 32, 42 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β πΊ ππΉβ) |
44 | | rexex 3077 |
. . . . . . . . . . . . . . 15
β’
(ββ β
πΊ ππΉβ β ββ ππΉβ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ ππΉβ) |
46 | 12, 45 | cpcoll2d 43018 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β (πΉ Coll π§)ππΉβ) |
47 | 28 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β πΊ β Univ) |
48 | 35 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π§ β πΊ) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β π§ β πΊ) |
50 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΊ) β πΊ β Univ) |
51 | | grumnudlem.3 |
. . . . . . . . . . . . . . . . . . . 20
β’ πΉ = ({β¨π, πβ© β£ βπ(βͺ π = π β§ π β π β§ π β π)} β© (πΊ Γ πΊ)) |
52 | | inss2 4230 |
. . . . . . . . . . . . . . . . . . . 20
β’
({β¨π, πβ© β£ βπ(βͺ
π = π β§ π β π β§ π β π)} β© (πΊ Γ πΊ)) β (πΊ Γ πΊ) |
53 | 51, 52 | eqsstri 4017 |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ β (πΊ Γ πΊ) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΊ) β πΉ β (πΊ Γ πΊ)) |
55 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΊ) β π§ β πΊ) |
56 | 50, 54, 55 | grucollcld 43019 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β πΊ) β (πΉ Coll π§) β πΊ) |
57 | 27, 49, 56 | syl2an2r 684 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β (πΉ Coll π§) β πΊ) |
58 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β β β (πΉ Coll π§)) |
59 | | gruel 10798 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β Univ β§ (πΉ Coll π§) β πΊ β§ β β (πΉ Coll π§)) β β β πΊ) |
60 | 47, 57, 58, 59 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β β β πΊ) |
61 | 39, 60, 40 | syl2an2r 684 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) |
62 | 61 | rexbidva 3177 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β (ββ β (πΉ Coll π§)ππΉβ β ββ β (πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π))) |
63 | 46, 62 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β (πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π)) |
64 | | rexcom4 3286 |
. . . . . . . . . . . . 13
β’
(ββ β
(πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π) β βπββ β (πΉ Coll π§)(βͺ π = β β§ π β π β§ π β π)) |
65 | | grumnudlem.5 |
. . . . . . . . . . . . . . 15
β’ ((β β (πΉ Coll π§) β§ (βͺ π = β β§ π β π β§ π β π)) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
66 | 65 | rexlimiva 3148 |
. . . . . . . . . . . . . 14
β’
(ββ β
(πΉ Coll π§)(βͺ π = β β§ π β π β§ π β π) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
67 | 66 | exlimiv 1934 |
. . . . . . . . . . . . 13
β’
(βπββ β (πΉ Coll π§)(βͺ π = β β§ π β π β§ π β π) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
68 | 64, 67 | sylbi 216 |
. . . . . . . . . . . 12
β’
(ββ β
(πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
69 | 63, 68 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
70 | | elssuni 4942 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ π’
β (πΉ Coll π§) β βͺ π’
β βͺ (πΉ Coll π§)) |
71 | | ssun2 4174 |
. . . . . . . . . . . . . . . . 17
β’ βͺ (πΉ
Coll π§) β (π«
π§ βͺ βͺ (πΉ
Coll π§)) |
72 | 70, 71 | sstrdi 3995 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π’
β (πΉ Coll π§) β βͺ π’
β (π« π§ βͺ
βͺ (πΉ Coll π§))) |
73 | 72 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β§ βͺ π’ β (πΉ Coll π§)) β βͺ π’ β (π« π§ βͺ βͺ (πΉ
Coll π§))) |
74 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β§ βͺ π’ β (πΉ Coll π§)) β π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) |
75 | 73, 74 | sseqtrrd 4024 |
. . . . . . . . . . . . . 14
β’ ((π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β§ βͺ π’ β (πΉ Coll π§)) β βͺ π’ β π€) |
76 | 75 | ex 414 |
. . . . . . . . . . . . 13
β’ (π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β (βͺ π’ β (πΉ Coll π§) β βͺ π’ β π€)) |
77 | 76 | anim2d 613 |
. . . . . . . . . . . 12
β’ (π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β ((π β π’ β§ βͺ π’ β (πΉ Coll π§)) β (π β π’ β§ βͺ π’ β π€))) |
78 | 77 | reximdv 3171 |
. . . . . . . . . . 11
β’ (π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β (βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§)) β βπ’ β π (π β π’ β§ βͺ π’ β π€))) |
79 | 11, 69, 78 | sylc 65 |
. . . . . . . . . 10
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β βπ’ β π (π β π’ β§ βͺ π’ β π€)) |
80 | 79 | rexlimdv3a 3160 |
. . . . . . . . 9
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))) |
81 | 80 | ralrimiva 3147 |
. . . . . . . 8
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))) |
82 | 10, 81 | jca 513 |
. . . . . . 7
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
83 | 82 | 3expa 1119 |
. . . . . 6
β’ (((π β§ π§ β πΊ) β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
84 | | grupw 10790 |
. . . . . . . 8
β’ ((πΊ β Univ β§ π§ β πΊ) β π« π§ β πΊ) |
85 | 1, 84 | sylan 581 |
. . . . . . 7
β’ ((π β§ π§ β πΊ) β π« π§ β πΊ) |
86 | | gruuni 10795 |
. . . . . . . 8
β’ ((πΊ β Univ β§ (πΉ Coll π§) β πΊ) β βͺ (πΉ Coll π§) β πΊ) |
87 | 1, 56, 86 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ π§ β πΊ) β βͺ (πΉ Coll π§) β πΊ) |
88 | | gruun 10801 |
. . . . . . 7
β’ ((πΊ β Univ β§ π«
π§ β πΊ β§ βͺ (πΉ Coll π§) β πΊ) β (π« π§ βͺ βͺ (πΉ Coll π§)) β πΊ) |
89 | 50, 85, 87, 88 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π§ β πΊ) β (π« π§ βͺ βͺ (πΉ Coll π§)) β πΊ) |
90 | 83, 89 | rspcime 3617 |
. . . . 5
β’ ((π β§ π§ β πΊ) β βπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
91 | 90 | alrimiv 1931 |
. . . 4
β’ ((π β§ π§ β πΊ) β βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
92 | 7, 91 | jca 513 |
. . 3
β’ ((π β§ π§ β πΊ) β (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) |
93 | 92 | ralrimiva 3147 |
. 2
β’ (π β βπ§ β πΊ (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) |
94 | | grumnudlem.1 |
. . . 4
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} |
95 | 94 | ismnu 43020 |
. . 3
β’ (πΊ β Univ β (πΊ β π β βπ§ β πΊ (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))))) |
96 | 1, 95 | syl 17 |
. 2
β’ (π β (πΊ β π β βπ§ β πΊ (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))))) |
97 | 93, 96 | mpbird 257 |
1
β’ (π β πΊ β π) |