Theorem stm1i

Description: State of component of unit meet. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	⊢ 𝐴 ∈ Cℋ
	stle.2	⊢ 𝐵 ∈ Cℋ
Assertion	stm1i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		stle.1	⊢ 𝐴 ∈ Cℋ
2		stle.2	⊢ 𝐵 ∈ Cℋ
3		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
4	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
5	4 1	stlei	⊢ ( 𝑆 ∈ States → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( 𝑆 ‘ 𝐴 ) ) )
6	3 5	mpi	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( 𝑆 ‘ 𝐴 ) )
7		breq1	⊢ ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( 𝑆 ‘ 𝐴 ) ↔ 1 ≤ ( 𝑆 ‘ 𝐴 ) ) )
8	6 7	syl5ibcom	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → 1 ≤ ( 𝑆 ‘ 𝐴 ) ) )
9	1	stge1i	⊢ ( 𝑆 ∈ States → ( 1 ≤ ( 𝑆 ‘ 𝐴 ) ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )
10	8 9	sylibd	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) )