Theorem lowerss ≪ | index | src | ≫

theorem lowerss (A: set): $ lower A C_ A $;


finite A <-> A == lower A
A == lower A -> lower A C_ A
finite A -> lower A C_ A
0 C_ A
~finite A -> lower A = 0
~finite A -> lower A == 0
~finite A -> (lower A C_ A <-> 0 C_ A)
~finite A -> lower A C_ A
lower A C_ A

Step	Hyp	Ref	Expression
1		eqlower	finite A <-> A == lower A
2		eqssr	A == lower A -> lower A C_ A
3	1, 2	sylbi	finite A -> lower A C_ A
4		ss01	0 C_ A
5		lower0	~finite A -> lower A = 0
6	5	nseqd	~finite A -> lower A == 0
7	6	sseq1d	~finite A -> (lower A C_ A <-> 0 C_ A)
8	4, 7	mpbiri	~finite A -> lower A C_ A
9	3, 8	cases	lower A C_ A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)