Theorem ococss

Description: Inclusion in complement of complement. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	ococss	⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ ) )
2		ocorth	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑦 ·ih 𝑥 ) = 0 ) )
3	2	expd	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) → ( 𝑦 ·ih 𝑥 ) = 0 ) ) )
4	3	ralrimdv	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑦 ·ih 𝑥 ) = 0 ) )
5	1 4	jcad	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → ( 𝑦 ∈ ℋ ∧ ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑦 ·ih 𝑥 ) = 0 ) ) )
6		ocss	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
7		ocel	⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ → ( 𝑦 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( 𝑦 ∈ ℋ ∧ ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑦 ·ih 𝑥 ) = 0 ) ) )
8	6 7	syl	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( 𝑦 ∈ ℋ ∧ ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑦 ·ih 𝑥 ) = 0 ) ) )
9	5 8	sylibrd	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
10	9	ssrdv	⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )