Metamath Proof Explorer


Theorem strle1

Description: Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypotheses strle1.i I
strle1.a A = I
Assertion strle1 A X Struct I I

Proof

Step Hyp Ref Expression
1 strle1.i I
2 strle1.a A = I
3 1 nnrei I
4 3 leidi I I
5 1 1 4 3pm3.2i I I I I
6 difss A X A X
7 2 1 eqeltri A
8 funsng A X V Fun A X
9 7 8 mpan X V Fun A X
10 funss A X A X Fun A X Fun A X
11 6 9 10 mpsyl X V Fun A X
12 fun0 Fun
13 opprc2 ¬ X V A X =
14 13 sneqd ¬ X V A X =
15 14 difeq1d ¬ X V A X =
16 difid =
17 15 16 eqtrdi ¬ X V A X =
18 17 funeqd ¬ X V Fun A X Fun
19 12 18 mpbiri ¬ X V Fun A X
20 11 19 pm2.61i Fun A X
21 dmsnopss dom A X A
22 2 sneqi A = I
23 1 nnzi I
24 fzsn I I I = I
25 23 24 ax-mp I I = I
26 22 25 eqtr4i A = I I
27 21 26 sseqtri dom A X I I
28 isstruct A X Struct I I I I I I Fun A X dom A X I I
29 5 20 27 28 mpbir3an A X Struct I I