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	syl6eq	|- ( -. 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 >.