This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )