Theorem stcltrlem2

Description: Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stcltr1.1	⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
	stcltr1.2	⊢ 𝐴 ∈ Cℋ
	stcltrlem1.3	⊢ 𝐵 ∈ Cℋ
Assertion	stcltrlem2	⊢ ( 𝜑 → 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stcltr1.1	⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
2		stcltr1.2	⊢ 𝐴 ∈ Cℋ
3		stcltrlem1.3	⊢ 𝐵 ∈ Cℋ
4	1 2 3	stcltrlem1	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) = 1 → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = 1 ) )
5	2	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
6	2 3	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
7	5 6	chjcli	⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ
8	1 3 7	stcltr1i	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐵 ) = 1 → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = 1 ) → 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
9	4 8	mpd	⊢ ( 𝜑 → 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )