Theorem axins2prim 4096

Description: ax-ins2 4085 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)

Assertion

Ref	Expression
axins2prim	⊢ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = 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

Step	Hyp	Ref	Expression
1		ax-ins2 4085	. 2 ⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
2		df-clel 2349	. . . . . . 7 ⊢ (⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ∃a(a = ⟪{{z}}, ⟪w, t⟫⟫ ∧ a ∈ y))
3		axprimlem2 4090	. . . . . . . . . 10 ⊢ (a = ⟪{{z}}, ⟪w, t⟫⟫ ↔ ∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = {{z}}) ∨ ∀f(f ∈ b ↔ (f = {{z}} ∨ f = ⟪w, t⟫)))))
4		axprimlem1 4089	. . . . . . . . . . . . . . . 16 ⊢ (c = {{z}} ↔ ∀d(d ∈ c ↔ d = {z}))
5		axprimlem1 4089	. . . . . . . . . . . . . . . . . 18 ⊢ (d = {z} ↔ ∀e(e ∈ d ↔ e = z))
6	5	bibi2i 304	. . . . . . . . . . . . . . . . 17 ⊢ ((d ∈ c ↔ d = {z}) ↔ (d ∈ c ↔ ∀e(e ∈ d ↔ e = z)))
7	6	albii 1566	. . . . . . . . . . . . . . . 16 ⊢ (∀d(d ∈ c ↔ d = {z}) ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z)))
8	4, 7	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (c = {{z}} ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z)))
9	8	bibi2i 304	. . . . . . . . . . . . . 14 ⊢ ((c ∈ b ↔ c = {{z}}) ↔ (c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))))
10	9	albii 1566	. . . . . . . . . . . . 13 ⊢ (∀c(c ∈ b ↔ c = {{z}}) ↔ ∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))))
11		axprimlem1 4089	. . . . . . . . . . . . . . . . 17 ⊢ (f = {{z}} ↔ ∀g(g ∈ f ↔ g = {z}))
12		axprimlem1 4089	. . . . . . . . . . . . . . . . . . 19 ⊢ (g = {z} ↔ ∀e(e ∈ g ↔ e = z))
13	12	bibi2i 304	. . . . . . . . . . . . . . . . . 18 ⊢ ((g ∈ f ↔ g = {z}) ↔ (g ∈ f ↔ ∀e(e ∈ g ↔ e = z)))
14	13	albii 1566	. . . . . . . . . . . . . . . . 17 ⊢ (∀g(g ∈ f ↔ g = {z}) ↔ ∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)))
15	11, 14	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ (f = {{z}} ↔ ∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)))
16		axprimlem2 4090	. . . . . . . . . . . . . . . 16 ⊢ (f = ⟪w, t⟫ ↔ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))
17	15, 16	orbi12i 507	. . . . . . . . . . . . . . 15 ⊢ ((f = {{z}} ∨ f = ⟪w, t⟫) ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t))))))
18	17	bibi2i 304	. . . . . . . . . . . . . 14 ⊢ ((f ∈ b ↔ (f = {{z}} ∨ f = ⟪w, t⟫)) ↔ (f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))
19	18	albii 1566	. . . . . . . . . . . . 13 ⊢ (∀f(f ∈ b ↔ (f = {{z}} ∨ f = ⟪w, t⟫)) ↔ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))
20	10, 19	orbi12i 507	. . . . . . . . . . . 12 ⊢ ((∀c(c ∈ b ↔ c = {{z}}) ∨ ∀f(f ∈ b ↔ (f = {{z}} ∨ f = ⟪w, t⟫))) ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t))))))))
21	20	bibi2i 304	. . . . . . . . . . 11 ⊢ ((b ∈ a ↔ (∀c(c ∈ b ↔ c = {{z}}) ∨ ∀f(f ∈ b ↔ (f = {{z}} ∨ f = ⟪w, t⟫)))) ↔ (b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))))
22	21	albii 1566	. . . . . . . . . 10 ⊢ (∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = {{z}}) ∨ ∀f(f ∈ b ↔ (f = {{z}} ∨ f = ⟪w, t⟫)))) ↔ ∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))))
23	3, 22	bitri 240	. . . . . . . . 9 ⊢ (a = ⟪{{z}}, ⟪w, t⟫⟫ ↔ ∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))))
24	23	anbi1i 676	. . . . . . . 8 ⊢ ((a = ⟪{{z}}, ⟪w, t⟫⟫ ∧ a ∈ y) ↔ (∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y))
25	24	exbii 1582	. . . . . . 7 ⊢ (∃a(a = ⟪{{z}}, ⟪w, t⟫⟫ ∧ a ∈ y) ↔ ∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y))
26	2, 25	bitri 240	. . . . . 6 ⊢ (⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y))
27		df-clel 2349	. . . . . . 7 ⊢ (⟪z, t⟫ ∈ x ↔ ∃k(k = ⟪z, t⟫ ∧ k ∈ x))
28		axprimlem2 4090	. . . . . . . . 9 ⊢ (k = ⟪z, t⟫ ↔ ∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))))
29	28	anbi1i 676	. . . . . . . 8 ⊢ ((k = ⟪z, t⟫ ∧ k ∈ x) ↔ (∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x))
30	29	exbii 1582	. . . . . . 7 ⊢ (∃k(k = ⟪z, t⟫ ∧ k ∈ x) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x))
31	27, 30	bitri 240	. . . . . 6 ⊢ (⟪z, t⟫ ∈ x ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x))
32	26, 31	bibi12i 306	. . . . 5 ⊢ ((⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) ↔ (∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x)))
33	32	albii 1566	. . . 4 ⊢ (∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) ↔ ∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x)))
34	33	2albii 1567	. . 3 ⊢ (∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) ↔ ∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x)))
35	34	exbii 1582	. 2 ⊢ (∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) ↔ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x)))
36	1, 35	mpbi 199	1 ⊢ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x))

Syntax hints:   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {csn 3738  ⟪copk 4058

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 4085

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 2479  df-v 2862  df-nin 3212  df-compl 3213  df-un 3215  df-sn 3742  df-pr 3743  df-opk 4059

This theorem is referenced by: (None)