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

Theorem enpw1lem1 6061
 Description: Lemma for enpw1 6062. Set up stratification for the reverse direction. (Contributed by SF, 26-Feb-2015.)
Assertion
Ref Expression
enpw1lem1 {x, y {x}g{y}} V
Distinct variable group:   x,g,y

Proof of Theorem enpw1lem1
Dummy variables a b p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . 6 x V
2 vex 2862 . . . . . 6 y V
31, 2opex 4588 . . . . 5 x, y V
43eluni1 4173 . . . 4 (x, y 1((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) ↔ {x, y} ((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g))
5 elima 4754 . . . . 5 ({x, y} ((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) ↔ p g p(( SI 1st 1st ) ∩ ( SI 2nd 2nd )){x, y})
6 brin 4693 . . . . . . 7 (p(( SI 1st 1st ) ∩ ( SI 2nd 2nd )){x, y} ↔ (p( SI 1st 1st ){x, y} p( SI 2nd 2nd ){x, y}))
7 brco 4883 . . . . . . . . 9 (p( SI 1st 1st ){x, y} ↔ a(p1st a a SI 1st {x, y}))
8 ancom 437 . . . . . . . . . . 11 ((p1st a a SI 1st {x, y}) ↔ (a SI 1st {x, y} p1st a))
93brsnsi2 5776 . . . . . . . . . . . . 13 (a SI 1st {x, y} ↔ b(a = {b} b1st x, y))
10 ancom 437 . . . . . . . . . . . . . . 15 ((a = {b} b1st x, y) ↔ (b1st x, y a = {b}))
11 brcnv 4892 . . . . . . . . . . . . . . . . 17 (b1st x, yx, y1st b)
121, 2opbr1st 5501 . . . . . . . . . . . . . . . . 17 (x, y1st bx = b)
13 equcom 1680 . . . . . . . . . . . . . . . . 17 (x = bb = x)
1411, 12, 133bitri 262 . . . . . . . . . . . . . . . 16 (b1st x, yb = x)
1514anbi1i 676 . . . . . . . . . . . . . . 15 ((b1st x, y a = {b}) ↔ (b = x a = {b}))
1610, 15bitri 240 . . . . . . . . . . . . . 14 ((a = {b} b1st x, y) ↔ (b = x a = {b}))
1716exbii 1582 . . . . . . . . . . . . 13 (b(a = {b} b1st x, y) ↔ b(b = x a = {b}))
18 sneq 3744 . . . . . . . . . . . . . . 15 (b = x → {b} = {x})
1918eqeq2d 2364 . . . . . . . . . . . . . 14 (b = x → (a = {b} ↔ a = {x}))
201, 19ceqsexv 2894 . . . . . . . . . . . . 13 (b(b = x a = {b}) ↔ a = {x})
219, 17, 203bitri 262 . . . . . . . . . . . 12 (a SI 1st {x, y} ↔ a = {x})
2221anbi1i 676 . . . . . . . . . . 11 ((a SI 1st {x, y} p1st a) ↔ (a = {x} p1st a))
238, 22bitri 240 . . . . . . . . . 10 ((p1st a a SI 1st {x, y}) ↔ (a = {x} p1st a))
2423exbii 1582 . . . . . . . . 9 (a(p1st a a SI 1st {x, y}) ↔ a(a = {x} p1st a))
25 snex 4111 . . . . . . . . . 10 {x} V
26 breq2 4643 . . . . . . . . . 10 (a = {x} → (p1st ap1st {x}))
2725, 26ceqsexv 2894 . . . . . . . . 9 (a(a = {x} p1st a) ↔ p1st {x})
287, 24, 273bitri 262 . . . . . . . 8 (p( SI 1st 1st ){x, y} ↔ p1st {x})
29 brco 4883 . . . . . . . . 9 (p( SI 2nd 2nd ){x, y} ↔ a(p2nd a a SI 2nd {x, y}))
303brsnsi2 5776 . . . . . . . . . . . . 13 (a SI 2nd {x, y} ↔ b(a = {b} b2nd x, y))
31 brcnv 4892 . . . . . . . . . . . . . . . . 17 (b2nd x, yx, y2nd b)
321, 2opbr2nd 5502 . . . . . . . . . . . . . . . . 17 (x, y2nd by = b)
33 equcom 1680 . . . . . . . . . . . . . . . . 17 (y = bb = y)
3431, 32, 333bitri 262 . . . . . . . . . . . . . . . 16 (b2nd x, yb = y)
3534anbi2i 675 . . . . . . . . . . . . . . 15 ((a = {b} b2nd x, y) ↔ (a = {b} b = y))
36 ancom 437 . . . . . . . . . . . . . . 15 ((a = {b} b = y) ↔ (b = y a = {b}))
3735, 36bitri 240 . . . . . . . . . . . . . 14 ((a = {b} b2nd x, y) ↔ (b = y a = {b}))
3837exbii 1582 . . . . . . . . . . . . 13 (b(a = {b} b2nd x, y) ↔ b(b = y a = {b}))
39 sneq 3744 . . . . . . . . . . . . . . 15 (b = y → {b} = {y})
4039eqeq2d 2364 . . . . . . . . . . . . . 14 (b = y → (a = {b} ↔ a = {y}))
412, 40ceqsexv 2894 . . . . . . . . . . . . 13 (b(b = y a = {b}) ↔ a = {y})
4230, 38, 413bitri 262 . . . . . . . . . . . 12 (a SI 2nd {x, y} ↔ a = {y})
4342anbi2i 675 . . . . . . . . . . 11 ((p2nd a a SI 2nd {x, y}) ↔ (p2nd a a = {y}))
44 ancom 437 . . . . . . . . . . 11 ((p2nd a a = {y}) ↔ (a = {y} p2nd a))
4543, 44bitri 240 . . . . . . . . . 10 ((p2nd a a SI 2nd {x, y}) ↔ (a = {y} p2nd a))
4645exbii 1582 . . . . . . . . 9 (a(p2nd a a SI 2nd {x, y}) ↔ a(a = {y} p2nd a))
47 snex 4111 . . . . . . . . . 10 {y} V
48 breq2 4643 . . . . . . . . . 10 (a = {y} → (p2nd ap2nd {y}))
4947, 48ceqsexv 2894 . . . . . . . . 9 (a(a = {y} p2nd a) ↔ p2nd {y})
5029, 46, 493bitri 262 . . . . . . . 8 (p( SI 2nd 2nd ){x, y} ↔ p2nd {y})
5128, 50anbi12i 678 . . . . . . 7 ((p( SI 1st 1st ){x, y} p( SI 2nd 2nd ){x, y}) ↔ (p1st {x} p2nd {y}))
5225, 47op1st2nd 5790 . . . . . . 7 ((p1st {x} p2nd {y}) ↔ p = {x}, {y})
536, 51, 523bitri 262 . . . . . 6 (p(( SI 1st 1st ) ∩ ( SI 2nd 2nd )){x, y} ↔ p = {x}, {y})
5453rexbii 2639 . . . . 5 (p g p(( SI 1st 1st ) ∩ ( SI 2nd 2nd )){x, y} ↔ p g p = {x}, {y})
555, 54bitri 240 . . . 4 ({x, y} ((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) ↔ p g p = {x}, {y})
56 df-br 4640 . . . . 5 ({x}g{y} ↔ {x}, {y} g)
57 risset 2661 . . . . 5 ({x}, {y} gp g p = {x}, {y})
5856, 57bitr2i 241 . . . 4 (p g p = {x}, {y} ↔ {x}g{y})
594, 55, 583bitri 262 . . 3 (x, y 1((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) ↔ {x}g{y})
6059opabbi2i 4866 . 2 1((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) = {x, y {x}g{y}}
61 1stex 4739 . . . . . . . 8 1st V
6261cnvex 5102 . . . . . . 7 1st V
6362siex 4753 . . . . . 6 SI 1st V
6463, 61coex 4750 . . . . 5 ( SI 1st 1st ) V
65 2ndex 5112 . . . . . . . 8 2nd V
6665cnvex 5102 . . . . . . 7 2nd V
6766siex 4753 . . . . . 6 SI 2nd V
6867, 65coex 4750 . . . . 5 ( SI 2nd 2nd ) V
6964, 68inex 4105 . . . 4 (( SI 1st 1st ) ∩ ( SI 2nd 2nd )) V
70 vex 2862 . . . 4 g V
7169, 70imaex 4747 . . 3 ((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) V
7271uni1ex 4293 . 2 1((( SI 1st 1st ) ∩ ( SI 2nd 2nd )) “ g) V
7360, 72eqeltrri 2424 1 {x, y {x}g{y}} V
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2615  Vcvv 2859   ∩ cin 3208  {csn 3737  ⋃1cuni1 4133  ⟨cop 4561  {copab 4622   class class class wbr 4639  1st c1st 4717   SI csi 4720   ∘ ccom 4721   “ cima 4722  ◡ccnv 4771  2nd c2nd 4783 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-co 4726  df-ima 4727  df-si 4728  df-cnv 4785  df-2nd 4797 This theorem is referenced by:  enpw1  6062
 Copyright terms: Public domain W3C validator