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⟩\} \cup \{⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨oc (ndx), \underset{˙}{⊥}⟩\}) Struct ⟨1, 11⟩$

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		basendx	$⊢ {Base}_{ndx} = 1$
3		1lt9	$⊢ 1 < 9$
4		9nn	$⊢ 9 \in ℕ$
5		tsetndx	$⊢ TopSet (ndx) = 9$
6	1 2 3 4 5	strle2	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨TopSet (ndx), J⟩\} Struct ⟨1, 9⟩$
7		10nn	$⊢ 10 \in ℕ$
8		plendx	$⊢ \leq_{ndx} = 10$
9		1nn0	$⊢ 1 \in ℕ_{0}$
10		0nn0	$⊢ 0 \in ℕ_{0}$
11		0lt1	$⊢ 0 < 1$
12	9 10 1 11	declt	$⊢ 10 < 11$
13	9 1	decnncl	$⊢ 11 \in ℕ$
14		ocndx	$⊢ oc (ndx) = 11$
15	7 8 12 13 14	strle2	$⊢ \{⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨oc (ndx), \underset{˙}{⊥}⟩\} Struct ⟨10, 11⟩$
16		9lt10	$⊢ 9 < 10$
17	6 15 16	strleun	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨TopSet (ndx), J⟩\} \cup \{⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨oc (ndx), \underset{˙}{⊥}⟩\}) Struct ⟨1, 11⟩$

Metamath Proof Explorer