Theorem ipostr

Description: The structure of df-ipo is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015)

	Ref	Expression
Assertion	ipostr	|- ( { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ._|_ >. } ) Struct <. 1 , ; 1 1 >.

Proof

Step	Hyp	Ref	Expression
1		1nn	|- 1 e. NN
2		basendx	|- ( Base ` ndx ) = 1
3		1lt9	|- 1 < 9
4		9nn	|- 9 e. NN
5		tsetndx	|- ( TopSet ` ndx ) = 9
6	1 2 3 4 5	strle2	|- { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. } Struct <. 1 , 9 >.
7		10nn	|- ; 1 0 e. NN
8		plendx	|- ( le ` ndx ) = ; 1 0
9		1nn0	|- 1 e. NN0
10		0nn0	|- 0 e. NN0
11		0lt1	|- 0 < 1
12	9 10 1 11	declt	|- ; 1 0 < ; 1 1
13	9 1	decnncl	|- ; 1 1 e. NN
14		ocndx	|- ( oc ` ndx ) = ; 1 1
15	7 8 12 13 14	strle2	|- { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ._|_ >. } Struct <. ; 1 0 , ; 1 1 >.
16		9lt10	|- 9 < ; 1 0
17	6 15 16	strleun	|- ( { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ._|_ >. } ) Struct <. 1 , ; 1 1 >.