![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > strleund | Unicode version |
Description: Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Ref | Expression |
---|---|
strleund.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
strleund.g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
strleund.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
strleund |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | strleund.f |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | isstructim 11562 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simp1d 956 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | simp1d 956 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | strleund.g |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | isstructim 11562 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | syl 14 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | simp1d 956 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | simp2d 957 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 5 | nnred 8489 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 9 | simp1d 956 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12 | nnred 8489 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 10 | nnred 8489 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 4 | simp2d 957 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15 | nnred 8489 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 4 | simp3d 958 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | strleund.l |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 16, 13, 18 | ltled 7656 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 11, 16, 13, 17, 19 | letrd 7661 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 9 | simp3d 958 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | 11, 13, 14, 20, 21 | letrd 7661 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
23 | 3 | simp2d 957 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 8 | simp2d 957 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | difss 3127 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
26 | dmss 4648 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
27 | 25, 26 | mp1i 10 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | 3 | simp3d 958 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 27, 28 | sstrd 3036 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | difss 3127 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
31 | dmss 4648 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
32 | 30, 31 | mp1i 10 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 8 | simp3d 958 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 32, 33 | sstrd 3036 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | ss2in 3228 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
36 | 29, 34, 35 | syl2anc 404 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | fzdisj 9520 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
38 | 18, 37 | syl 14 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | sseq0 3328 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
40 | 36, 38, 39 | syl2anc 404 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | funun 5071 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
42 | 23, 24, 40, 41 | syl21anc 1174 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | difundir 3253 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
44 | 43 | funeqi 5049 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
45 | 42, 44 | sylibr 133 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | structex 11560 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
47 | 1, 46 | syl 14 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
48 | structex 11560 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
49 | 6, 48 | syl 14 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
50 | unexg 4278 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
51 | 47, 49, 50 | syl2anc 404 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | dmun 4656 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
53 | 15 | nnzd 8921 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
54 | 10 | nnzd 8921 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
55 | 16, 13, 14, 19, 21 | letrd 7661 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
56 | eluz2 9079 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
57 | 53, 54, 55, 56 | syl3anbrc 1128 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
58 | fzss2 9532 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
59 | 57, 58 | syl 14 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
60 | 28, 59 | sstrd 3036 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
61 | 5 | nnzd 8921 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
62 | 12 | nnzd 8921 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
63 | eluz2 9079 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
64 | 61, 62, 20, 63 | syl3anbrc 1128 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
65 | fzss1 9531 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
66 | 64, 65 | syl 14 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
67 | 33, 66 | sstrd 3036 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
68 | 60, 67 | unssd 3177 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
69 | 52, 68 | syl5eqss 3071 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
70 | isstructr 11563 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
71 | 5, 10, 22, 45, 51, 69, 70 | syl33anc 1190 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-13 1450 ax-14 1451 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3963 ax-pow 4015 ax-pr 4045 ax-un 4269 ax-setind 4366 ax-cnex 7490 ax-resscn 7491 ax-1cn 7492 ax-1re 7493 ax-icn 7494 ax-addcl 7495 ax-addrcl 7496 ax-mulcl 7497 ax-addcom 7499 ax-addass 7501 ax-distr 7503 ax-i2m1 7504 ax-0lt1 7505 ax-0id 7507 ax-rnegex 7508 ax-cnre 7510 ax-pre-ltirr 7511 ax-pre-ltwlin 7512 ax-pre-lttrn 7513 ax-pre-ltadd 7515 |
This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-fal 1296 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ne 2257 df-nel 2352 df-ral 2365 df-rex 2366 df-reu 2367 df-rab 2369 df-v 2622 df-sbc 2842 df-dif 3002 df-un 3004 df-in 3006 df-ss 3013 df-nul 3288 df-pw 3435 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-int 3695 df-br 3852 df-opab 3906 df-mpt 3907 df-id 4129 df-xp 4457 df-rel 4458 df-cnv 4459 df-co 4460 df-dm 4461 df-rn 4462 df-res 4463 df-ima 4464 df-iota 4993 df-fun 5030 df-fn 5031 df-f 5032 df-fv 5036 df-riota 5622 df-ov 5669 df-oprab 5670 df-mpt2 5671 df-pnf 7578 df-mnf 7579 df-xr 7580 df-ltxr 7581 df-le 7582 df-sub 7709 df-neg 7710 df-inn 8477 df-n0 8728 df-z 8805 df-uz 9074 df-fz 9479 df-struct 11550 |
This theorem is referenced by: strle2g 11639 strle3g 11640 srngstrd 11670 lmodstrd 11681 ipsstrd 11689 |
Copyright terms: Public domain | W3C validator |