Description: The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | insubm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | submrcl | |
|
2 | ssinss1 | |
|
3 | 2 | 3ad2ant1 | |
4 | 3 | ad2antrl | |
5 | elin | |
|
6 | 5 | simplbi2com | |
7 | 6 | 3ad2ant2 | |
8 | 7 | com12 | |
9 | 8 | 3ad2ant2 | |
10 | 9 | imp | |
11 | 10 | adantl | |
12 | elin | |
|
13 | elin | |
|
14 | 12 13 | anbi12i | |
15 | oveq1 | |
|
16 | 15 | eleq1d | |
17 | oveq2 | |
|
18 | 17 | eleq1d | |
19 | simpl | |
|
20 | 19 | adantr | |
21 | eqidd | |
|
22 | simpl | |
|
23 | 22 | adantl | |
24 | 16 18 20 21 23 | rspc2vd | |
25 | 24 | com12 | |
26 | 25 | 3ad2ant3 | |
27 | 26 | ad2antrl | |
28 | 27 | imp | |
29 | 15 | eleq1d | |
30 | 17 | eleq1d | |
31 | simpr | |
|
32 | 31 | adantr | |
33 | eqidd | |
|
34 | simpr | |
|
35 | 34 | adantl | |
36 | 29 30 32 33 35 | rspc2vd | |
37 | 36 | com12 | |
38 | 37 | 3ad2ant3 | |
39 | 38 | adantl | |
40 | 39 | adantl | |
41 | 40 | imp | |
42 | 28 41 | elind | |
43 | 42 | ex | |
44 | 14 43 | syl5bi | |
45 | 44 | ralrimivv | |
46 | 4 11 45 | 3jca | |
47 | 46 | ex | |
48 | eqid | |
|
49 | eqid | |
|
50 | eqid | |
|
51 | 48 49 50 | issubm | |
52 | 48 49 50 | issubm | |
53 | 51 52 | anbi12d | |
54 | 48 49 50 | issubm | |
55 | 47 53 54 | 3imtr4d | |
56 | 55 | expd | |
57 | 1 56 | mpcom | |
58 | 57 | imp | |