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

Theorem eqpw1relk 4479
 Description: Represent equality to unit power class via a Kuratowski relationship. (Contributed by SF, 21-Jan-2015.)
Hypotheses
Ref Expression
eqpw1relk.1 A V
eqpw1relk.2 B V
Assertion
Ref Expression
eqpw1relk (⟪A, {B}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ A = 1B)

Proof of Theorem eqpw1relk
Dummy variables x t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . . 5 {B} V
2 eqpw1relk.1 . . . . . 6 A V
32, 1opkelxpk 4248 . . . . 5 (⟪A, {B}⟫ (1c ×k V) ↔ (A 1c {B} V))
41, 3mpbiran2 885 . . . 4 (⟪A, {B}⟫ (1c ×k V) ↔ A 1c)
52elpw 3728 . . . 4 (A 1cA 1c)
64, 5bitri 240 . . 3 (⟪A, {B}⟫ (1c ×k V) ↔ A 1c)
7 opkex 4113 . . . . . . 7 A, {B}⟫ V
87elimak 4259 . . . . . 6 (⟪A, {B}⟫ (( Ins3k SkIns2k SIk Sk ) “k 1111c) ↔ t 1 111ct, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ))
9 elpw131c 4149 . . . . . . . . . 10 (t 1111cx t = {{{{x}}}})
109anbi1i 676 . . . . . . . . 9 ((t 1111c t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ (x t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
11 19.41v 1901 . . . . . . . . 9 (x(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ (x t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
1210, 11bitr4i 243 . . . . . . . 8 ((t 1111c t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ x(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
1312exbii 1582 . . . . . . 7 (t(t 1111c t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ tx(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
14 df-rex 2620 . . . . . . 7 (t 1 111ct, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ t(t 1111c t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
15 excom 1741 . . . . . . 7 (xt(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ tx(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
1613, 14, 153bitr4i 268 . . . . . 6 (t 1 111ct, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ xt(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
178, 16bitri 240 . . . . 5 (⟪A, {B}⟫ (( Ins3k SkIns2k SIk Sk ) “k 1111c) ↔ xt(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
18 snex 4111 . . . . . . . 8 {{{{x}}}} V
19 opkeq1 4059 . . . . . . . . 9 (t = {{{{x}}}} → ⟪t, ⟪A, {B}⟫⟫ = ⟪{{{{x}}}}, ⟪A, {B}⟫⟫)
2019eleq1d 2419 . . . . . . . 8 (t = {{{{x}}}} → (⟪t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
2118, 20ceqsexv 2894 . . . . . . 7 (t(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ))
22 elsymdif 3223 . . . . . . . 8 (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ ¬ (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins3k Sk ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins2k SIk Sk ))
23 snex 4111 . . . . . . . . . . 11 {{x}} V
2423, 2, 1otkelins3k 4256 . . . . . . . . . 10 (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins3k Sk ↔ ⟪{{x}}, A Sk )
25 snex 4111 . . . . . . . . . . 11 {x} V
2625, 2elssetk 4270 . . . . . . . . . 10 (⟪{{x}}, A Sk ↔ {x} A)
2724, 26bitri 240 . . . . . . . . 9 (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins3k Sk ↔ {x} A)
2823, 2, 1otkelins2k 4255 . . . . . . . . . 10 (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins2k SIk Sk ↔ ⟪{{x}}, {B}⟫ SIk Sk )
29 eqpw1relk.2 . . . . . . . . . . . 12 B V
3025, 29opksnelsik 4265 . . . . . . . . . . 11 (⟪{{x}}, {B}⟫ SIk Sk ↔ ⟪{x}, B Sk )
31 vex 2862 . . . . . . . . . . . 12 x V
3231, 29elssetk 4270 . . . . . . . . . . 11 (⟪{x}, B Skx B)
3330, 32bitri 240 . . . . . . . . . 10 (⟪{{x}}, {B}⟫ SIk Skx B)
3428, 33bitri 240 . . . . . . . . 9 (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins2k SIk Skx B)
3527, 34bibi12i 306 . . . . . . . 8 ((⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins3k Sk ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ Ins2k SIk Sk ) ↔ ({x} Ax B))
3622, 35xchbinx 301 . . . . . . 7 (⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ ¬ ({x} Ax B))
3721, 36bitri 240 . . . . . 6 (t(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ ¬ ({x} Ax B))
3837exbii 1582 . . . . 5 (xt(t = {{{{x}}}} t, ⟪A, {B}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ x ¬ ({x} Ax B))
39 exnal 1574 . . . . 5 (x ¬ ({x} Ax B) ↔ ¬ x({x} Ax B))
4017, 38, 393bitrri 263 . . . 4 x({x} Ax B) ↔ ⟪A, {B}⟫ (( Ins3k SkIns2k SIk Sk ) “k 1111c))
4140con1bii 321 . . 3 (¬ ⟪A, {B}⟫ (( Ins3k SkIns2k SIk Sk ) “k 1111c) ↔ x({x} Ax B))
426, 41anbi12i 678 . 2 ((⟪A, {B}⟫ (1c ×k V) ¬ ⟪A, {B}⟫ (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ (A 1c x({x} Ax B)))
43 eldif 3221 . 2 (⟪A, {B}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ (⟪A, {B}⟫ (1c ×k V) ¬ ⟪A, {B}⟫ (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
44 eqpw1 4162 . 2 (A = 1B ↔ (A 1c x({x} Ax B)))
4542, 43, 443bitr4i 268 1 (⟪A, {B}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ A = 1B)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2615  Vcvv 2859   ∖ cdif 3206   ⊕ csymdif 3209   ⊆ wss 3257  ℘cpw 3722  {csn 3737  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-pw 3724  df-sn 3741  df-pr 3742  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-sik 4192  df-ssetk 4193 This theorem is referenced by:  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  srelk  4524
 Copyright terms: Public domain W3C validator