stlesi

Description: Ordering law for states. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	$⊢ A \in C_{ℋ}$
	stle.2	$⊢ B \in C_{ℋ}$
Assertion	stlesi	$⊢ S \in States \to (A \subseteq B \to (S (A) = 1 \to S (B) = 1))$

Step	Hyp	Ref	Expression
1		stle.1	$⊢ A \in C_{ℋ}$
2		stle.2	$⊢ B \in C_{ℋ}$
3		stle1	$⊢ S \in States \to (B \in C_{ℋ} \to S (B) \leq 1)$
4	2 3	mpi	$⊢ S \in States \to S (B) \leq 1$
5	4	adantr	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to S (B) \leq 1$
6	1 2	stlei	$⊢ S \in States \to (A \subseteq B \to S (A) \leq S (B))$
7	6	imp	$⊢ (S \in States \land A \subseteq B) \to S (A) \leq S (B)$
8	7	adantrr	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to S (A) \leq S (B)$
9		breq1	$⊢ S (A) = 1 \to (S (A) \leq S (B) \leftrightarrow 1 \leq S (B))$
10	9	ad2antll	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to (S (A) \leq S (B) \leftrightarrow 1 \leq S (B))$
11	8 10	mpbid	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to 1 \leq S (B)$
12		stcl	$⊢ S \in States \to (B \in C_{ℋ} \to S (B) \in ℝ)$
13	2 12	mpi	$⊢ S \in States \to S (B) \in ℝ$
14		1re	$⊢ 1 \in ℝ$
15	13 14	jctir	$⊢ S \in States \to (S (B) \in ℝ \land 1 \in ℝ)$
16	15	adantr	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to (S (B) \in ℝ \land 1 \in ℝ)$
17		letri3	$⊢ (S (B) \in ℝ \land 1 \in ℝ) \to (S (B) = 1 \leftrightarrow (S (B) \leq 1 \land 1 \leq S (B)))$
18	16 17	syl	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to (S (B) = 1 \leftrightarrow (S (B) \leq 1 \land 1 \leq S (B)))$
19	5 11 18	mpbir2and	$⊢ (S \in States \land (A \subseteq B \land S (A) = 1)) \to S (B) = 1$
20	19	exp32	$⊢ S \in States \to (A \subseteq B \to (S (A) = 1 \to S (B) = 1))$

Metamath Proof Explorer