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

Theorem insklem 4304
Description: Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of (11c ×k (V ×k V)). (Contributed by SF, 14-Jan-2015.)
Hypotheses
Ref Expression
insklem.1 A (11c ×k (V ×k V))
insklem.2 B (11c ×k (V ×k V))
Assertion
Ref Expression
insklem (A = Bxyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
Distinct variable groups:   x,A,y,z   x,B,y,z

Proof of Theorem insklem
Dummy variables w t u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 insklem.1 . . 3 A (11c ×k (V ×k V))
2 insklem.2 . . 3 B (11c ×k (V ×k V))
3 ssofeq 4077 . . 3 ((A (11c ×k (V ×k V)) B (11c ×k (V ×k V))) → (A = Bw (11c ×k (V ×k V))(w Aw B)))
41, 2, 3mp2an 653 . 2 (A = Bw (11c ×k (V ×k V))(w Aw B))
5 19.23v 1891 . . . . 5 (x(yz w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ (xyz w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
6 19.23vv 1892 . . . . . 6 (yz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ (yz w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
76albii 1566 . . . . 5 (xyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ x(yz w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
8 19.42vv 1907 . . . . . . . . . 10 (yz(t 11c u = ⟪y, z⟫) ↔ (t 11c yz u = ⟪y, z⟫))
98anbi2i 675 . . . . . . . . 9 ((w = ⟪t, u yz(t 11c u = ⟪y, z⟫)) ↔ (w = ⟪t, u (t 11c yz u = ⟪y, z⟫)))
10 19.42vv 1907 . . . . . . . . 9 (yz(w = ⟪t, u (t 11c u = ⟪y, z⟫)) ↔ (w = ⟪t, u yz(t 11c u = ⟪y, z⟫)))
11 elvvk 4207 . . . . . . . . . . 11 (u (V ×k V) ↔ yz u = ⟪y, z⟫)
1211anbi2i 675 . . . . . . . . . 10 ((t 11c u (V ×k V)) ↔ (t 11c yz u = ⟪y, z⟫))
1312anbi2i 675 . . . . . . . . 9 ((w = ⟪t, u (t 11c u (V ×k V))) ↔ (w = ⟪t, u (t 11c yz u = ⟪y, z⟫)))
149, 10, 133bitr4ri 269 . . . . . . . 8 ((w = ⟪t, u (t 11c u (V ×k V))) ↔ yz(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
15142exbii 1583 . . . . . . 7 (tu(w = ⟪t, u (t 11c u (V ×k V))) ↔ tuyz(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
16 elxpk 4196 . . . . . . 7 (w (11c ×k (V ×k V)) ↔ tu(w = ⟪t, u (t 11c u (V ×k V))))
17 exrot3 1744 . . . . . . . 8 (xyz w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ yzx w = ⟪{{x}}, ⟪y, z⟫⟫)
18 exancom 1586 . . . . . . . . . . . 12 (t(w = ⟪t, ⟪y, z⟫⟫ t 11c) ↔ t(t 11c w = ⟪t, ⟪y, z⟫⟫))
19 elpw11c 4147 . . . . . . . . . . . . . . 15 (t 11cx t = {{x}})
2019anbi1i 676 . . . . . . . . . . . . . 14 ((t 11c w = ⟪t, ⟪y, z⟫⟫) ↔ (x t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
21 19.41v 1901 . . . . . . . . . . . . . 14 (x(t = {{x}} w = ⟪t, ⟪y, z⟫⟫) ↔ (x t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
2220, 21bitr4i 243 . . . . . . . . . . . . 13 ((t 11c w = ⟪t, ⟪y, z⟫⟫) ↔ x(t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
2322exbii 1582 . . . . . . . . . . . 12 (t(t 11c w = ⟪t, ⟪y, z⟫⟫) ↔ tx(t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
2418, 23bitri 240 . . . . . . . . . . 11 (t(w = ⟪t, ⟪y, z⟫⟫ t 11c) ↔ tx(t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
25 ancom 437 . . . . . . . . . . . . . . 15 ((t 11c u = ⟪y, z⟫) ↔ (u = ⟪y, z t 11c))
2625anbi2i 675 . . . . . . . . . . . . . 14 ((w = ⟪t, u (t 11c u = ⟪y, z⟫)) ↔ (w = ⟪t, u (u = ⟪y, z t 11c)))
27 an12 772 . . . . . . . . . . . . . 14 ((w = ⟪t, u (u = ⟪y, z t 11c)) ↔ (u = ⟪y, z (w = ⟪t, u t 11c)))
2826, 27bitri 240 . . . . . . . . . . . . 13 ((w = ⟪t, u (t 11c u = ⟪y, z⟫)) ↔ (u = ⟪y, z (w = ⟪t, u t 11c)))
29282exbii 1583 . . . . . . . . . . . 12 (tu(w = ⟪t, u (t 11c u = ⟪y, z⟫)) ↔ tu(u = ⟪y, z (w = ⟪t, u t 11c)))
30 opkex 4113 . . . . . . . . . . . . . 14 y, z V
31 opkeq2 4060 . . . . . . . . . . . . . . . 16 (u = ⟪y, z⟫ → ⟪t, u⟫ = ⟪t, ⟪y, z⟫⟫)
3231eqeq2d 2364 . . . . . . . . . . . . . . 15 (u = ⟪y, z⟫ → (w = ⟪t, u⟫ ↔ w = ⟪t, ⟪y, z⟫⟫))
3332anbi1d 685 . . . . . . . . . . . . . 14 (u = ⟪y, z⟫ → ((w = ⟪t, u t 11c) ↔ (w = ⟪t, ⟪y, z⟫⟫ t 11c)))
3430, 33ceqsexv 2894 . . . . . . . . . . . . 13 (u(u = ⟪y, z (w = ⟪t, u t 11c)) ↔ (w = ⟪t, ⟪y, z⟫⟫ t 11c))
3534exbii 1582 . . . . . . . . . . . 12 (tu(u = ⟪y, z (w = ⟪t, u t 11c)) ↔ t(w = ⟪t, ⟪y, z⟫⟫ t 11c))
3629, 35bitri 240 . . . . . . . . . . 11 (tu(w = ⟪t, u (t 11c u = ⟪y, z⟫)) ↔ t(w = ⟪t, ⟪y, z⟫⟫ t 11c))
37 snex 4111 . . . . . . . . . . . . . 14 {{x}} V
38 opkeq1 4059 . . . . . . . . . . . . . . 15 (t = {{x}} → ⟪t, ⟪y, z⟫⟫ = ⟪{{x}}, ⟪y, z⟫⟫)
3938eqeq2d 2364 . . . . . . . . . . . . . 14 (t = {{x}} → (w = ⟪t, ⟪y, z⟫⟫ ↔ w = ⟪{{x}}, ⟪y, z⟫⟫))
4037, 39ceqsexv 2894 . . . . . . . . . . . . 13 (t(t = {{x}} w = ⟪t, ⟪y, z⟫⟫) ↔ w = ⟪{{x}}, ⟪y, z⟫⟫)
4140exbii 1582 . . . . . . . . . . . 12 (xt(t = {{x}} w = ⟪t, ⟪y, z⟫⟫) ↔ x w = ⟪{{x}}, ⟪y, z⟫⟫)
42 excom 1741 . . . . . . . . . . . 12 (xt(t = {{x}} w = ⟪t, ⟪y, z⟫⟫) ↔ tx(t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
4341, 42bitr3i 242 . . . . . . . . . . 11 (x w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ tx(t = {{x}} w = ⟪t, ⟪y, z⟫⟫))
4424, 36, 433bitr4ri 269 . . . . . . . . . 10 (x w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ tu(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
45442exbii 1583 . . . . . . . . 9 (yzx w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ yztu(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
46 exrot4 1745 . . . . . . . . 9 (yztu(w = ⟪t, u (t 11c u = ⟪y, z⟫)) ↔ tuyz(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
4745, 46bitri 240 . . . . . . . 8 (yzx w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ tuyz(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
4817, 47bitri 240 . . . . . . 7 (xyz w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ tuyz(w = ⟪t, u (t 11c u = ⟪y, z⟫)))
4915, 16, 483bitr4i 268 . . . . . 6 (w (11c ×k (V ×k V)) ↔ xyz w = ⟪{{x}}, ⟪y, z⟫⟫)
5049imbi1i 315 . . . . 5 ((w (11c ×k (V ×k V)) → (w Aw B)) ↔ (xyz w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
515, 7, 503bitr4ri 269 . . . 4 ((w (11c ×k (V ×k V)) → (w Aw B)) ↔ xyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
5251albii 1566 . . 3 (w(w (11c ×k (V ×k V)) → (w Aw B)) ↔ wxyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
53 df-ral 2619 . . 3 (w (11c ×k (V ×k V))(w Aw B) ↔ w(w (11c ×k (V ×k V)) → (w Aw B)))
54 alcom 1737 . . . 4 (wxyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ xwyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
55 alrot3 1738 . . . . 5 (wyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ yzw(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
5655albii 1566 . . . 4 (xwyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ xyzw(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
57 opkex 4113 . . . . . . 7 ⟪{{x}}, ⟪y, z⟫⟫ V
58 eleq1 2413 . . . . . . . 8 (w = ⟪{{x}}, ⟪y, z⟫⟫ → (w A ↔ ⟪{{x}}, ⟪y, z⟫⟫ A))
59 eleq1 2413 . . . . . . . 8 (w = ⟪{{x}}, ⟪y, z⟫⟫ → (w B ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
6058, 59bibi12d 312 . . . . . . 7 (w = ⟪{{x}}, ⟪y, z⟫⟫ → ((w Aw B) ↔ (⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B)))
6157, 60ceqsalv 2885 . . . . . 6 (w(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ (⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
6261albii 1566 . . . . 5 (zw(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ z(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
63622albii 1567 . . . 4 (xyzw(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)) ↔ xyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
6454, 56, 633bitrri 263 . . 3 (xyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B) ↔ wxyz(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w Aw B)))
6552, 53, 643bitr4i 268 . 2 (w (11c ×k (V ×k V))(w Aw B) ↔ xyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
664, 65bitri 240 1 (A = Bxyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  wral 2614  Vcvv 2859   wss 3257  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174
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-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-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
This theorem is referenced by:  ins2kexg  4305  ins3kexg  4306
  Copyright terms: Public domain W3C validator