Metamath Proof Explorer


Theorem occon

Description: Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion occon A B A B B A

Proof

Step Hyp Ref Expression
1 ssralv A B y B x ih y = 0 y A x ih y = 0
2 1 adantr A B x y B x ih y = 0 y A x ih y = 0
3 2 ss2rabdv A B x | y B x ih y = 0 x | y A x ih y = 0
4 3 adantl A B A B x | y B x ih y = 0 x | y A x ih y = 0
5 ocval B B = x | y B x ih y = 0
6 5 ad2antlr A B A B B = x | y B x ih y = 0
7 ocval A A = x | y A x ih y = 0
8 7 ad2antrr A B A B A = x | y A x ih y = 0
9 4 6 8 3sstr4d A B A B B A
10 9 ex A B A B B A