Step | Hyp | Ref
| Expression |
1 | | grumnudlem.2 |
. . . . . . . 8
β’ (π β πΊ β Univ) |
2 | | gruss 10793 |
. . . . . . . 8
β’ ((πΊ β Univ β§ π§ β πΊ β§ π β π§) β π β πΊ) |
3 | 1, 2 | syl3an1 1161 |
. . . . . . 7
β’ ((π β§ π§ β πΊ β§ π β π§) β π β πΊ) |
4 | 3 | 3expia 1119 |
. . . . . 6
β’ ((π β§ π§ β πΊ) β (π β π§ β π β πΊ)) |
5 | 4 | alrimiv 1928 |
. . . . 5
β’ ((π β§ π§ β πΊ) β βπ(π β π§ β π β πΊ)) |
6 | | pwss 4624 |
. . . . 5
β’
(π« π§ β
πΊ β βπ(π β π§ β π β πΊ)) |
7 | 5, 6 | sylibr 233 |
. . . 4
β’ ((π β§ π§ β πΊ) β π« π§ β πΊ) |
8 | | ssun1 4171 |
. . . . . . . . 9
β’ π«
π§ β (π« π§ βͺ βͺ (πΉ
Coll π§)) |
9 | | simp3 1136 |
. . . . . . . . 9
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) |
10 | 8, 9 | sseqtrrid 4034 |
. . . . . . . 8
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β π« π§ β π€) |
11 | | simp1l3 1266 |
. . . . . . . . . . 11
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) |
12 | | simp1r 1196 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π β π§) |
13 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β = βͺ
π£ β§ π = π£) β π = π£) |
14 | 13 | unieqd 4921 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β = βͺ
π£ β§ π = π£) β βͺ π = βͺ
π£) |
15 | | simpl 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β = βͺ
π£ β§ π = π£) β β = βͺ π£) |
16 | 14, 15 | eqtr4d 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β = βͺ
π£ β§ π = π£) β βͺ π = β) |
17 | 16 | adantll 710 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β βͺ π = β) |
18 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π = π£) |
19 | | simpll3 1212 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β (π β π£ β§ π£ β π)) |
20 | 19 | simprd 494 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π£ β π) |
21 | 18, 20 | eqeltrd 2831 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π β π) |
22 | 19 | simpld 493 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π β π£) |
23 | 22, 18 | eleqtrrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β π β π) |
24 | 17, 21, 23 | 3jca 1126 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β§ π = π£) β (βͺ π = β β§ π β π β§ π β π)) |
25 | | simpl2 1190 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β π£ β πΊ) |
26 | 24, 25 | rr-spce 43258 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β = βͺ π£) β βπ(βͺ
π = β β§ π β π β§ π β π)) |
27 | | simp1l1 1264 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π) |
28 | 27, 1 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β πΊ β Univ) |
29 | | simp2 1135 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π£ β πΊ) |
30 | | gruuni 10797 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β Univ β§ π£ β πΊ) β βͺ π£ β πΊ) |
31 | 28, 29, 30 | syl2anc 582 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β βͺ π£ β πΊ) |
32 | 26, 31 | rspcime 3615 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β πΊ βπ(βͺ π = β β§ π β π β§ π β π)) |
33 | | simpl1 1189 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π) |
34 | 33, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β πΊ β Univ) |
35 | | simpl2 1190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π§ β πΊ) |
36 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π β π§) |
37 | | gruel 10800 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ β Univ β§ π§ β πΊ β§ π β π§) β π β πΊ) |
38 | 34, 35, 36, 37 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β π β πΊ) |
39 | 38 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π β πΊ) |
40 | | grumnudlem.4 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β πΊ β§ β β πΊ) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) |
41 | 39, 40 | sylan 578 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β πΊ) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) |
42 | 41 | rexbidva 3174 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β (ββ β πΊ ππΉβ β ββ β πΊ βπ(βͺ π = β β§ π β π β§ π β π))) |
43 | 32, 42 | mpbird 256 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β πΊ ππΉβ) |
44 | | rexex 3074 |
. . . . . . . . . . . . . . 15
β’
(ββ β
πΊ ππΉβ β ββ ππΉβ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ ππΉβ) |
46 | 12, 45 | cpcoll2d 43320 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β (πΉ Coll π§)ππΉβ) |
47 | 28 | adantr 479 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β πΊ β Univ) |
48 | 35 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β π§ β πΊ) |
49 | 48 | adantr 479 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β π§ β πΊ) |
50 | 1 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΊ) β πΊ β Univ) |
51 | | grumnudlem.3 |
. . . . . . . . . . . . . . . . . . . 20
β’ πΉ = ({β¨π, πβ© β£ βπ(βͺ π = π β§ π β π β§ π β π)} β© (πΊ Γ πΊ)) |
52 | | inss2 4228 |
. . . . . . . . . . . . . . . . . . . 20
β’
({β¨π, πβ© β£ βπ(βͺ
π = π β§ π β π β§ π β π)} β© (πΊ Γ πΊ)) β (πΊ Γ πΊ) |
53 | 51, 52 | eqsstri 4015 |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ β (πΊ Γ πΊ) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΊ) β πΉ β (πΊ Γ πΊ)) |
55 | | simpr 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΊ) β π§ β πΊ) |
56 | 50, 54, 55 | grucollcld 43321 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β πΊ) β (πΉ Coll π§) β πΊ) |
57 | 27, 49, 56 | syl2an2r 681 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β (πΉ Coll π§) β πΊ) |
58 | | simpr 483 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β β β (πΉ Coll π§)) |
59 | | gruel 10800 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β Univ β§ (πΉ Coll π§) β πΊ β§ β β (πΉ Coll π§)) β β β πΊ) |
60 | 47, 57, 58, 59 | syl3anc 1369 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β β β πΊ) |
61 | 39, 60, 40 | syl2an2r 681 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β§ β β (πΉ Coll π§)) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) |
62 | 61 | rexbidva 3174 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β (ββ β (πΉ Coll π§)ππΉβ β ββ β (πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π))) |
63 | 46, 62 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β ββ β (πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π)) |
64 | | rexcom4 3283 |
. . . . . . . . . . . . 13
β’
(ββ β
(πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π) β βπββ β (πΉ Coll π§)(βͺ π = β β§ π β π β§ π β π)) |
65 | | grumnudlem.5 |
. . . . . . . . . . . . . . 15
β’ ((β β (πΉ Coll π§) β§ (βͺ π = β β§ π β π β§ π β π)) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
66 | 65 | rexlimiva 3145 |
. . . . . . . . . . . . . 14
β’
(ββ β
(πΉ Coll π§)(βͺ π = β β§ π β π β§ π β π) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
67 | 66 | exlimiv 1931 |
. . . . . . . . . . . . 13
β’
(βπββ β (πΉ Coll π§)(βͺ π = β β§ π β π β§ π β π) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
68 | 64, 67 | sylbi 216 |
. . . . . . . . . . . 12
β’
(ββ β
(πΉ Coll π§)βπ(βͺ π = β β§ π β π β§ π β π) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
69 | 63, 68 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) |
70 | | elssuni 4940 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ π’
β (πΉ Coll π§) β βͺ π’
β βͺ (πΉ Coll π§)) |
71 | | ssun2 4172 |
. . . . . . . . . . . . . . . . 17
β’ βͺ (πΉ
Coll π§) β (π«
π§ βͺ βͺ (πΉ
Coll π§)) |
72 | 70, 71 | sstrdi 3993 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π’
β (πΉ Coll π§) β βͺ π’
β (π« π§ βͺ
βͺ (πΉ Coll π§))) |
73 | 72 | adantl 480 |
. . . . . . . . . . . . . . 15
β’ ((π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β§ βͺ π’ β (πΉ Coll π§)) β βͺ π’ β (π« π§ βͺ βͺ (πΉ
Coll π§))) |
74 | | simpl 481 |
. . . . . . . . . . . . . . 15
β’ ((π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β§ βͺ π’ β (πΉ Coll π§)) β π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) |
75 | 73, 74 | sseqtrrd 4022 |
. . . . . . . . . . . . . 14
β’ ((π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β§ βͺ π’ β (πΉ Coll π§)) β βͺ π’ β π€) |
76 | 75 | ex 411 |
. . . . . . . . . . . . 13
β’ (π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β (βͺ π’ β (πΉ Coll π§) β βͺ π’ β π€)) |
77 | 76 | anim2d 610 |
. . . . . . . . . . . 12
β’ (π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β ((π β π’ β§ βͺ π’ β (πΉ Coll π§)) β (π β π’ β§ βͺ π’ β π€))) |
78 | 77 | reximdv 3168 |
. . . . . . . . . . 11
β’ (π€ = (π« π§ βͺ βͺ (πΉ Coll π§)) β (βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§)) β βπ’ β π (π β π’ β§ βͺ π’ β π€))) |
79 | 11, 69, 78 | sylc 65 |
. . . . . . . . . 10
β’ ((((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β§ π£ β πΊ β§ (π β π£ β§ π£ β π)) β βπ’ β π (π β π’ β§ βͺ π’ β π€)) |
80 | 79 | rexlimdv3a 3157 |
. . . . . . . . 9
β’ (((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β§ π β π§) β (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))) |
81 | 80 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))) |
82 | 10, 81 | jca 510 |
. . . . . . 7
β’ ((π β§ π§ β πΊ β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
83 | 82 | 3expa 1116 |
. . . . . 6
β’ (((π β§ π§ β πΊ) β§ π€ = (π« π§ βͺ βͺ (πΉ Coll π§))) β (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
84 | | grupw 10792 |
. . . . . . . 8
β’ ((πΊ β Univ β§ π§ β πΊ) β π« π§ β πΊ) |
85 | 1, 84 | sylan 578 |
. . . . . . 7
β’ ((π β§ π§ β πΊ) β π« π§ β πΊ) |
86 | | gruuni 10797 |
. . . . . . . 8
β’ ((πΊ β Univ β§ (πΉ Coll π§) β πΊ) β βͺ (πΉ Coll π§) β πΊ) |
87 | 1, 56, 86 | syl2an2r 681 |
. . . . . . 7
β’ ((π β§ π§ β πΊ) β βͺ (πΉ Coll π§) β πΊ) |
88 | | gruun 10803 |
. . . . . . 7
β’ ((πΊ β Univ β§ π«
π§ β πΊ β§ βͺ (πΉ Coll π§) β πΊ) β (π« π§ βͺ βͺ (πΉ Coll π§)) β πΊ) |
89 | 50, 85, 87, 88 | syl3anc 1369 |
. . . . . 6
β’ ((π β§ π§ β πΊ) β (π« π§ βͺ βͺ (πΉ Coll π§)) β πΊ) |
90 | 83, 89 | rspcime 3615 |
. . . . 5
β’ ((π β§ π§ β πΊ) β βπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
91 | 90 | alrimiv 1928 |
. . . 4
β’ ((π β§ π§ β πΊ) β βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) |
92 | 7, 91 | jca 510 |
. . 3
β’ ((π β§ π§ β πΊ) β (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) |
93 | 92 | ralrimiva 3144 |
. 2
β’ (π β βπ§ β πΊ (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) |
94 | | grumnudlem.1 |
. . . 4
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} |
95 | 94 | ismnu 43322 |
. . 3
β’ (πΊ β Univ β (πΊ β π β βπ§ β πΊ (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))))) |
96 | 1, 95 | syl 17 |
. 2
β’ (π β (πΊ β π β βπ§ β πΊ (π« π§ β πΊ β§ βπβπ€ β πΊ (π« π§ β π€ β§ βπ β π§ (βπ£ β πΊ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))))) |
97 | 93, 96 | mpbird 256 |
1
β’ (π β πΊ β π) |