New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  opkltfing GIF version

Theorem opkltfing 4449
 Description: Kuratowski ordered pair membership in finite less than. (Contributed by SF, 27-Jan-2015.)
Assertion
Ref Expression
opkltfing ((A V B W) → (⟪A, B <fin ↔ (A x Nn B = ((A +c x) +c 1c))))
Distinct variable groups:   x,A   x,B
Allowed substitution hints:   V(x)   W(x)

Proof of Theorem opkltfing
Dummy variables w y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ltfin 4441 . 2 <fin = {y zw(y = ⟪z, w (z x Nn w = ((z +c x) +c 1c)))}
2 neeq1 2524 . . 3 (z = A → (zA))
3 addceq1 4383 . . . . . 6 (z = A → (z +c x) = (A +c x))
43addceq1d 4389 . . . . 5 (z = A → ((z +c x) +c 1c) = ((A +c x) +c 1c))
54eqeq2d 2364 . . . 4 (z = A → (w = ((z +c x) +c 1c) ↔ w = ((A +c x) +c 1c)))
65rexbidv 2635 . . 3 (z = A → (x Nn w = ((z +c x) +c 1c) ↔ x Nn w = ((A +c x) +c 1c)))
72, 6anbi12d 691 . 2 (z = A → ((z x Nn w = ((z +c x) +c 1c)) ↔ (A x Nn w = ((A +c x) +c 1c))))
8 eqeq1 2359 . . . 4 (w = B → (w = ((A +c x) +c 1c) ↔ B = ((A +c x) +c 1c)))
98rexbidv 2635 . . 3 (w = B → (x Nn w = ((A +c x) +c 1c) ↔ x Nn B = ((A +c x) +c 1c)))
109anbi2d 684 . 2 (w = B → ((A x Nn w = ((A +c x) +c 1c)) ↔ (A x Nn B = ((A +c x) +c 1c))))
111, 7, 10opkelopkabg 4245 1 ((A V B W) → (⟪A, B <fin ↔ (A x Nn B = ((A +c x) +c 1c))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  ∃wrex 2615  ∅c0 3550  ⟪copk 4057  1cc1c 4134   Nn cnnc 4373   +c cplc 4375
 Copyright terms: Public domain W3C validator