Theorem aceq5lem1 4715

Description: Lemma for aceq5 4720.

Assertion

Ref	Expression
aceq5lem1	⊢ (∃!v v ∈ (({w} × w) ∩ y) ↔ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y))

Distinct variable group:   w,v,y,g

Proof of Theorem aceq5lem1

Step	Hyp	Ref	Expression
1		elin 2203	. . . 4 ⊢ (v ∈ (({w} × w) ∩ y) ↔ (v ∈ ({w} × w) ⋀ v ∈ y))
2		elxp 3197	. . . . . 6 ⊢ (v ∈ ({w} × w) ↔ ∃t∃g(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)))
3		excom 1044	. . . . . 6 ⊢ (∃t∃g(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ↔ ∃g∃t(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)))
4	2, 3	bitr 173	. . . . 5 ⊢ (v ∈ ({w} × w) ↔ ∃g∃t(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)))
5	4	anbi1i 481	. . . 4 ⊢ ((v ∈ ({w} × w) ⋀ v ∈ y) ↔ (∃g∃t(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y))
6		19.41vv 1304	. . . . 5 ⊢ (∃g∃t((v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ (∃g∃t(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y))
7		an23 485	. . . . . . . . 9 ⊢ (((v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ ((v = ⟨t, g⟩ ⋀ v ∈ y) ⋀ (t ∈ {w} ⋀ g ∈ w)))
8		eleq1 1531	. . . . . . . . . . 11 ⊢ (v = ⟨t, g⟩ → (v ∈ y ↔ ⟨t, g⟩ ∈ y))
9	8	pm5.32i 644	. . . . . . . . . 10 ⊢ ((v = ⟨t, g⟩ ⋀ v ∈ y) ↔ (v = ⟨t, g⟩ ⋀ ⟨t, g⟩ ∈ y))
10		elsn 2417	. . . . . . . . . . 11 ⊢ (t ∈ {w} ↔ t = w)
11	10	anbi1i 481	. . . . . . . . . 10 ⊢ ((t ∈ {w} ⋀ g ∈ w) ↔ (t = w ⋀ g ∈ w))
12	9, 11	anbi12i 482	. . . . . . . . 9 ⊢ (((v = ⟨t, g⟩ ⋀ v ∈ y) ⋀ (t ∈ {w} ⋀ g ∈ w)) ↔ ((v = ⟨t, g⟩ ⋀ ⟨t, g⟩ ∈ y) ⋀ (t = w ⋀ g ∈ w)))
13		an4 506	. . . . . . . . . 10 ⊢ (((v = ⟨t, g⟩ ⋀ ⟨t, g⟩ ∈ y) ⋀ (t = w ⋀ g ∈ w)) ↔ ((v = ⟨t, g⟩ ⋀ t = w) ⋀ (⟨t, g⟩ ∈ y ⋀ g ∈ w)))
14		ancom 435	. . . . . . . . . . 11 ⊢ ((v = ⟨t, g⟩ ⋀ t = w) ↔ (t = w ⋀ v = ⟨t, g⟩))
15		ancom 435	. . . . . . . . . . 11 ⊢ ((⟨t, g⟩ ∈ y ⋀ g ∈ w) ↔ (g ∈ w ⋀ ⟨t, g⟩ ∈ y))
16	14, 15	anbi12i 482	. . . . . . . . . 10 ⊢ (((v = ⟨t, g⟩ ⋀ t = w) ⋀ (⟨t, g⟩ ∈ y ⋀ g ∈ w)) ↔ ((t = w ⋀ v = ⟨t, g⟩) ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y)))
17		anass 439	. . . . . . . . . 10 ⊢ (((t = w ⋀ v = ⟨t, g⟩) ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y)) ↔ (t = w ⋀ (v = ⟨t, g⟩ ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y))))
18	13, 16, 17	3bitr 177	. . . . . . . . 9 ⊢ (((v = ⟨t, g⟩ ⋀ ⟨t, g⟩ ∈ y) ⋀ (t = w ⋀ g ∈ w)) ↔ (t = w ⋀ (v = ⟨t, g⟩ ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y))))
19	7, 12, 18	3bitr 177	. . . . . . . 8 ⊢ (((v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ (t = w ⋀ (v = ⟨t, g⟩ ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y))))
20	19	exbii 1049	. . . . . . 7 ⊢ (∃t((v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ ∃t(t = w ⋀ (v = ⟨t, g⟩ ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y))))
21		visset 1809	. . . . . . . 8 ⊢ w ∈ V
22		opeq1 2483	. . . . . . . . . 10 ⊢ (t = w → ⟨t, g⟩ = ⟨w, g⟩)
23	22	eqeq2d 1483	. . . . . . . . 9 ⊢ (t = w → (v = ⟨t, g⟩ ↔ v = ⟨w, g⟩))
24	22	eleq1d 1537	. . . . . . . . . 10 ⊢ (t = w → (⟨t, g⟩ ∈ y ↔ ⟨w, g⟩ ∈ y))
25	24	anbi2d 615	. . . . . . . . 9 ⊢ (t = w → ((g ∈ w ⋀ ⟨t, g⟩ ∈ y) ↔ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
26	23, 25	anbi12d 627	. . . . . . . 8 ⊢ (t = w → ((v = ⟨t, g⟩ ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y)) ↔ (v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y))))
27	21, 26	ceqsexv 1831	. . . . . . 7 ⊢ (∃t(t = w ⋀ (v = ⟨t, g⟩ ⋀ (g ∈ w ⋀ ⟨t, g⟩ ∈ y))) ↔ (v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
28	20, 27	bitr 173	. . . . . 6 ⊢ (∃t((v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ (v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
29	28	exbii 1049	. . . . 5 ⊢ (∃g∃t((v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ ∃g(v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
30	6, 29	bitr3 175	. . . 4 ⊢ ((∃g∃t(v = ⟨t, g⟩ ⋀ (t ∈ {w} ⋀ g ∈ w)) ⋀ v ∈ y) ↔ ∃g(v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
31	1, 5, 30	3bitr 177	. . 3 ⊢ (v ∈ (({w} × w) ∩ y) ↔ ∃g(v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
32	31	eubii 1385	. 2 ⊢ (∃!v v ∈ (({w} × w) ∩ y) ↔ ∃!v∃g(v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
33		euop2 2801	. 2 ⊢ (∃!v∃g(v = ⟨w, g⟩ ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)) ↔ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y))
34	32, 33	bitr 173	1 ⊢ (∃!v v ∈ (({w} × w) ∩ y) ↔ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y))

Syntax hints:   ↔ wb 146   ⋀ wa 223   = wceq 954   ∈ wcel 956  ∃wex 978  ∃!weu 1378   ∩ cin 2042  {csn 2405  ⟨cop 2407   × cxp 3163

This theorem is referenced by:  aceq5lem5 4719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-opab 2662  df-xp 3179

Copyright terms: Public domain