Theorem stcltr2i

Description: Property of a strong classical state. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stcltr1.1	⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
	stcltr1.2	⊢ 𝐴 ∈ Cℋ
Assertion	stcltr2i	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) = 1 → 𝐴 = ℋ ) )

Proof

Step	Hyp	Ref	Expression
1		stcltr1.1	⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
2		stcltr1.2	⊢ 𝐴 ∈ Cℋ
3		ax-1	⊢ ( ( 𝑆 ‘ 𝐴 ) = 1 → ( ( 𝑆 ‘ ℋ ) = 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) )
4		helch	⊢ ℋ ∈ Cℋ
5	1 4 2	stcltr1i	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ℋ ) = 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) → ℋ ⊆ 𝐴 ) )
6	3 5	syl5	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) = 1 → ℋ ⊆ 𝐴 ) )
7	2	chssii	⊢ 𝐴 ⊆ ℋ
8		eqss	⊢ ( 𝐴 = ℋ ↔ ( 𝐴 ⊆ ℋ ∧ ℋ ⊆ 𝐴 ) )
9	7 8	mpbiran	⊢ ( 𝐴 = ℋ ↔ ℋ ⊆ 𝐴 )
10	6 9	imbitrrdi	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) = 1 → 𝐴 = ℋ ) )