Metamath Proof Explorer


Theorem wopprc

Description: Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion wopprc A V B V ¬ 1 𝑜 A B

Proof

Step Hyp Ref Expression
1 id = A = A
2 dfsn2 =
3 1 2 eqtr3di = A A =
4 snex A V
5 0ex V
6 4 5 preqr1 A = A =
7 3 6 syl = A A =
8 snprc ¬ A V A =
9 7 8 sylibr = A ¬ A V
10 8 biimpi ¬ A V A =
11 10 preq1d ¬ A V A =
12 2 11 eqtr4id ¬ A V = A
13 9 12 impbii = A ¬ A V
14 13 con2bii A V ¬ = A
15 snprc ¬ B V B =
16 eqcom B = = B
17 15 16 bitr2i = B ¬ B V
18 17 con2bii B V ¬ = B
19 5 sneqr = B = B
20 sneq = B = B
21 19 20 impbii = B = B
22 18 21 xchbinxr B V ¬ = B
23 14 22 anbi12i A V B V ¬ = A ¬ = B
24 pm4.56 ¬ = A ¬ = B ¬ = A = B
25 snex V
26 25 elpr A B = A = B
27 24 26 xchbinxr ¬ = A ¬ = B ¬ A B
28 23 27 bitri A V B V ¬ A B
29 df1o2 1 𝑜 =
30 29 eleq1i 1 𝑜 A B A B
31 28 30 xchbinxr A V B V ¬ 1 𝑜 A B