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

Theorem axins2prim 4095
 Description: ax-ins2 4084 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
Assertion
Ref Expression
axins2prim yzwt(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x))
Distinct variable groups:   a,b,t,w   y,a,z   b,c   f,b,t,w,z   c,d,z   e,d,z   e,g,z   f,g   f,h,t,w   z,f,g   h,i   h,j,t,w   w,i   t,j,w   k,l,t   x,k,z   m,l   n,l,t,z   z,m   t,n,z   w,t,x,y,z

Proof of Theorem axins2prim
StepHypRef Expression
1 ax-ins2 4084 . 2 yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x)
2 df-clel 2349 . . . . . . 7 (⟪{{z}}, ⟪w, t⟫⟫ ya(a = ⟪{{z}}, ⟪w, t⟫⟫ a y))
3 axprimlem2 4089 . . . . . . . . . 10 (a = ⟪{{z}}, ⟪w, t⟫⟫ ↔ b(b a ↔ (c(c bc = {{z}}) f(f b ↔ (f = {{z}} f = ⟪w, t⟫)))))
4 axprimlem1 4088 . . . . . . . . . . . . . . . 16 (c = {{z}} ↔ d(d cd = {z}))
5 axprimlem1 4088 . . . . . . . . . . . . . . . . . 18 (d = {z} ↔ e(e de = z))
65bibi2i 304 . . . . . . . . . . . . . . . . 17 ((d cd = {z}) ↔ (d ce(e de = z)))
76albii 1566 . . . . . . . . . . . . . . . 16 (d(d cd = {z}) ↔ d(d ce(e de = z)))
84, 7bitri 240 . . . . . . . . . . . . . . 15 (c = {{z}} ↔ d(d ce(e de = z)))
98bibi2i 304 . . . . . . . . . . . . . 14 ((c bc = {{z}}) ↔ (c bd(d ce(e de = z))))
109albii 1566 . . . . . . . . . . . . 13 (c(c bc = {{z}}) ↔ c(c bd(d ce(e de = z))))
11 axprimlem1 4088 . . . . . . . . . . . . . . . . 17 (f = {{z}} ↔ g(g fg = {z}))
12 axprimlem1 4088 . . . . . . . . . . . . . . . . . . 19 (g = {z} ↔ e(e ge = z))
1312bibi2i 304 . . . . . . . . . . . . . . . . . 18 ((g fg = {z}) ↔ (g fe(e ge = z)))
1413albii 1566 . . . . . . . . . . . . . . . . 17 (g(g fg = {z}) ↔ g(g fe(e ge = z)))
1511, 14bitri 240 . . . . . . . . . . . . . . . 16 (f = {{z}} ↔ g(g fe(e ge = z)))
16 axprimlem2 4089 . . . . . . . . . . . . . . . 16 (f = ⟪w, t⟫ ↔ h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))
1715, 16orbi12i 507 . . . . . . . . . . . . . . 15 ((f = {{z}} f = ⟪w, t⟫) ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t))))))
1817bibi2i 304 . . . . . . . . . . . . . 14 ((f b ↔ (f = {{z}} f = ⟪w, t⟫)) ↔ (f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))
1918albii 1566 . . . . . . . . . . . . 13 (f(f b ↔ (f = {{z}} f = ⟪w, t⟫)) ↔ f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))
2010, 19orbi12i 507 . . . . . . . . . . . 12 ((c(c bc = {{z}}) f(f b ↔ (f = {{z}} f = ⟪w, t⟫))) ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t))))))))
2120bibi2i 304 . . . . . . . . . . 11 ((b a ↔ (c(c bc = {{z}}) f(f b ↔ (f = {{z}} f = ⟪w, t⟫)))) ↔ (b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))))
2221albii 1566 . . . . . . . . . 10 (b(b a ↔ (c(c bc = {{z}}) f(f b ↔ (f = {{z}} f = ⟪w, t⟫)))) ↔ b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))))
233, 22bitri 240 . . . . . . . . 9 (a = ⟪{{z}}, ⟪w, t⟫⟫ ↔ b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))))
2423anbi1i 676 . . . . . . . 8 ((a = ⟪{{z}}, ⟪w, t⟫⟫ a y) ↔ (b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y))
2524exbii 1582 . . . . . . 7 (a(a = ⟪{{z}}, ⟪w, t⟫⟫ a y) ↔ a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y))
262, 25bitri 240 . . . . . 6 (⟪{{z}}, ⟪w, t⟫⟫ ya(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y))
27 df-clel 2349 . . . . . . 7 (⟪z, t xk(k = ⟪z, t k x))
28 axprimlem2 4089 . . . . . . . . 9 (k = ⟪z, t⟫ ↔ l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))))
2928anbi1i 676 . . . . . . . 8 ((k = ⟪z, t k x) ↔ (l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x))
3029exbii 1582 . . . . . . 7 (k(k = ⟪z, t k x) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x))
3127, 30bitri 240 . . . . . 6 (⟪z, t xk(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x))
3226, 31bibi12i 306 . . . . 5 ((⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x) ↔ (a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x)))
3332albii 1566 . . . 4 (t(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x) ↔ t(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x)))
34332albii 1567 . . 3 (zwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x) ↔ zwt(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x)))
3534exbii 1582 . 2 (yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x) ↔ yzwt(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x)))
361, 35mpbi 199 1 yzwt(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {csn 3737  ⟪copk 4057 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-ins2 4084 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-v 2861  df-nin 3211  df-compl 3212  df-un 3214  df-sn 3741  df-pr 3742  df-opk 4058 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator