Theorem wopprc

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

	Ref	Expression
Assertion	wopprc	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ¬ 1o ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( { ∅ } = { { 𝐴 } , ∅ } → { ∅ } = { { 𝐴 } , ∅ } )
2		dfsn2	⊢ { ∅ } = { ∅ , ∅ }
3	1 2	eqtr3di	⊢ ( { ∅ } = { { 𝐴 } , ∅ } → { { 𝐴 } , ∅ } = { ∅ , ∅ } )
4		snex	⊢ { 𝐴 } ∈ V
5		0ex	⊢ ∅ ∈ V
6	4 5	preqr1	⊢ ( { { 𝐴 } , ∅ } = { ∅ , ∅ } → { 𝐴 } = ∅ )
7	3 6	syl	⊢ ( { ∅ } = { { 𝐴 } , ∅ } → { 𝐴 } = ∅ )
8		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
9	7 8	sylibr	⊢ ( { ∅ } = { { 𝐴 } , ∅ } → ¬ 𝐴 ∈ V )
10	8	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
11	10	preq1d	⊢ ( ¬ 𝐴 ∈ V → { { 𝐴 } , ∅ } = { ∅ , ∅ } )
12	2 11	eqtr4id	⊢ ( ¬ 𝐴 ∈ V → { ∅ } = { { 𝐴 } , ∅ } )
13	9 12	impbii	⊢ ( { ∅ } = { { 𝐴 } , ∅ } ↔ ¬ 𝐴 ∈ V )
14	13	con2bii	⊢ ( 𝐴 ∈ V ↔ ¬ { ∅ } = { { 𝐴 } , ∅ } )
15		snprc	⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
16		eqcom	⊢ ( { 𝐵 } = ∅ ↔ ∅ = { 𝐵 } )
17	15 16	bitr2i	⊢ ( ∅ = { 𝐵 } ↔ ¬ 𝐵 ∈ V )
18	17	con2bii	⊢ ( 𝐵 ∈ V ↔ ¬ ∅ = { 𝐵 } )
19	5	sneqr	⊢ ( { ∅ } = { { 𝐵 } } → ∅ = { 𝐵 } )
20		sneq	⊢ ( ∅ = { 𝐵 } → { ∅ } = { { 𝐵 } } )
21	19 20	impbii	⊢ ( { ∅ } = { { 𝐵 } } ↔ ∅ = { 𝐵 } )
22	18 21	xchbinxr	⊢ ( 𝐵 ∈ V ↔ ¬ { ∅ } = { { 𝐵 } } )
23	14 22	anbi12i	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( ¬ { ∅ } = { { 𝐴 } , ∅ } ∧ ¬ { ∅ } = { { 𝐵 } } ) )
24		pm4.56	⊢ ( ( ¬ { ∅ } = { { 𝐴 } , ∅ } ∧ ¬ { ∅ } = { { 𝐵 } } ) ↔ ¬ ( { ∅ } = { { 𝐴 } , ∅ } ∨ { ∅ } = { { 𝐵 } } ) )
25		snex	⊢ { ∅ } ∈ V
26	25	elpr	⊢ ( { ∅ } ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } ↔ ( { ∅ } = { { 𝐴 } , ∅ } ∨ { ∅ } = { { 𝐵 } } ) )
27	24 26	xchbinxr	⊢ ( ( ¬ { ∅ } = { { 𝐴 } , ∅ } ∧ ¬ { ∅ } = { { 𝐵 } } ) ↔ ¬ { ∅ } ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } )
28	23 27	bitri	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ¬ { ∅ } ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } )
29		df1o2	⊢ 1o = { ∅ }
30	29	eleq1i	⊢ ( 1o ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } ↔ { ∅ } ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } )
31	28 30	xchbinxr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ¬ 1o ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } )