Theorem opprc1b 2810

Description: A property of an ordered pair of proper classes (due to our particular definition of ordered pair).

Assertion

Ref	Expression
opprc1b	⊢ (¬ A ∈ V ↔ ∅ ∈ ⟨A, B⟩)

Proof of Theorem opprc1b

Step	Hyp	Ref	Expression
1		opprc1 2510	. . 3 ⊢ (¬ A ∈ V → ⟨A, B⟩ = {∅, {B}})
2		0ex 2724	. . . 4 ⊢ ∅ ∈ V
3	2	prid1 2462	. . 3 ⊢ ∅ ∈ {∅, {B}}
4	1, 3	syl5eleqr 1562	. 2 ⊢ (¬ A ∈ V → ∅ ∈ ⟨A, B⟩)
5		opeq1 2499	. . . . . 6 ⊢ (x = A → ⟨x, B⟩ = ⟨A, B⟩)
6	5	eleq2d 1548	. . . . 5 ⊢ (x = A → (∅ ∈ ⟨x, B⟩ ↔ ∅ ∈ ⟨A, B⟩))
7	6	negbid 614	. . . 4 ⊢ (x = A → (¬ ∅ ∈ ⟨x, B⟩ ↔ ¬ ∅ ∈ ⟨A, B⟩))
8		visset 1820	. . . . . . . . 9 ⊢ x ∈ V
9	8	snnz 2470	. . . . . . . 8 ⊢ {x} ≠ ∅
10		df-ne 1594	. . . . . . . 8 ⊢ ({x} ≠ ∅ ↔ ¬ {x} = ∅)
11	9, 10	mpbi 189	. . . . . . 7 ⊢ ¬ {x} = ∅
12		eqcom 1484	. . . . . . 7 ⊢ ({x} = ∅ ↔ ∅ = {x})
13	11, 12	mtbi 191	. . . . . 6 ⊢ ¬ ∅ = {x}
14	8	prnz 2471	. . . . . . . 8 ⊢ {x, B} ≠ ∅
15		df-ne 1594	. . . . . . . 8 ⊢ ({x, B} ≠ ∅ ↔ ¬ {x, B} = ∅)
16	14, 15	mpbi 189	. . . . . . 7 ⊢ ¬ {x, B} = ∅
17		eqcom 1484	. . . . . . 7 ⊢ ({x, B} = ∅ ↔ ∅ = {x, B})
18	16, 17	mtbi 191	. . . . . 6 ⊢ ¬ ∅ = {x, B}
19	13, 18	pm3.2ni 583	. . . . 5 ⊢ ¬ (∅ = {x} ⋁ ∅ = {x, B})
20	2	elop 2797	. . . . 5 ⊢ (∅ ∈ ⟨x, B⟩ ↔ (∅ = {x} ⋁ ∅ = {x, B}))
21	19, 20	mtbir 192	. . . 4 ⊢ ¬ ∅ ∈ ⟨x, B⟩
22	7, 21	vtoclg 1854	. . 3 ⊢ (A ∈ V → ¬ ∅ ∈ ⟨A, B⟩)
23	22	con2i 97	. 2 ⊢ (∅ ∈ ⟨A, B⟩ → ¬ A ∈ V)
24	4, 23	impbi 157	1 ⊢ (¬ A ∈ V ↔ ∅ ∈ ⟨A, B⟩)

Syntax hints:  ¬ wn 2   ↔ wb 146   ⋁ wo 222   = wceq 960   ∈ wcel 962   ≠ wne 1592  Vcvv 1818  ∅c0 2289  {csn 2419  {cpr 2420  ⟨cop 2421

This theorem is referenced by:  opprc3 2811  opeqex 2812  opth2 2814  onxpdisj 3255  funopg 3561

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-nul 2723

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-v 1819  df-dif 2058  df-un 2059  df-nul 2290  df-sn 2422  df-pr 2423  df-op 2426

Copyright terms: Public domain