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 e. NN
strle1.a
|- A = I
Assertion strle1
|- { <. A , X >. } Struct <. I , I >.

Proof

Step Hyp Ref Expression
1 strle1.i
 |-  I e. NN
2 strle1.a
 |-  A = I
3 1 nnrei
 |-  I e. RR
4 3 leidi
 |-  I <_ I
5 1 1 4 3pm3.2i
 |-  ( I e. NN /\ I e. NN /\ I <_ I )
6 difss
 |-  ( { <. A , X >. } \ { (/) } ) C_ { <. A , X >. }
7 2 1 eqeltri
 |-  A e. NN
8 funsng
 |-  ( ( A e. NN /\ X e. _V ) -> Fun { <. A , X >. } )
9 7 8 mpan
 |-  ( X e. _V -> Fun { <. A , X >. } )
10 funss
 |-  ( ( { <. A , X >. } \ { (/) } ) C_ { <. A , X >. } -> ( Fun { <. A , X >. } -> Fun ( { <. A , X >. } \ { (/) } ) ) )
11 6 9 10 mpsyl
 |-  ( X e. _V -> Fun ( { <. A , X >. } \ { (/) } ) )
12 fun0
 |-  Fun (/)
13 opprc2
 |-  ( -. X e. _V -> <. A , X >. = (/) )
14 13 sneqd
 |-  ( -. X e. _V -> { <. A , X >. } = { (/) } )
15 14 difeq1d
 |-  ( -. X e. _V -> ( { <. A , X >. } \ { (/) } ) = ( { (/) } \ { (/) } ) )
16 difid
 |-  ( { (/) } \ { (/) } ) = (/)
17 15 16 eqtrdi
 |-  ( -. X e. _V -> ( { <. A , X >. } \ { (/) } ) = (/) )
18 17 funeqd
 |-  ( -. X e. _V -> ( Fun ( { <. A , X >. } \ { (/) } ) <-> Fun (/) ) )
19 12 18 mpbiri
 |-  ( -. X e. _V -> Fun ( { <. A , X >. } \ { (/) } ) )
20 11 19 pm2.61i
 |-  Fun ( { <. A , X >. } \ { (/) } )
21 dmsnopss
 |-  dom { <. A , X >. } C_ { A }
22 2 sneqi
 |-  { A } = { I }
23 1 nnzi
 |-  I e. ZZ
24 fzsn
 |-  ( I e. ZZ -> ( 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 >. } C_ ( I ... I )
28 isstruct
 |-  ( { <. A , X >. } Struct <. I , I >. <-> ( ( I e. NN /\ I e. NN /\ I <_ I ) /\ Fun ( { <. A , X >. } \ { (/) } ) /\ dom { <. A , X >. } C_ ( I ... I ) ) )
29 5 20 27 28 mpbir3an
 |-  { <. A , X >. } Struct <. I , I >.