Theorem stcltr1i

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ℋ
	stcltr1.3	⊢ 𝐵 ∈ Cℋ
Assertion	stcltr1i	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝐴 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		stcltr1.1	⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
2		stcltr1.2	⊢ 𝐴 ∈ Cℋ
3		stcltr1.3	⊢ 𝐵 ∈ Cℋ
4		fveqeq2	⊢ ( 𝑥 = 𝐴 → ( ( 𝑆 ‘ 𝑥 ) = 1 ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )
5	4	imbi1d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) ↔ ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) ) )
6		sseq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) )
7	5 6	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ↔ ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝐴 ⊆ 𝑦 ) ) )
8		fveqeq2	⊢ ( 𝑦 = 𝐵 → ( ( 𝑆 ‘ 𝑦 ) = 1 ↔ ( 𝑆 ‘ 𝐵 ) = 1 ) )
9	8	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) ↔ ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) ) )
10		sseq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝐵 ) )
11	9 10	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝐴 ⊆ 𝑦 ) ↔ ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝐴 ⊆ 𝐵 ) ) )
12	7 11	rspc2v	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) → ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝐴 ⊆ 𝐵 ) ) )
13	2 3 12	mp2an	⊢ ( ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) → ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝐴 ⊆ 𝐵 ) )
14	1 13	simplbiim	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝐴 ⊆ 𝐵 ) )