Theorem aceq5lem5 4722

Description: Lemma for aceq5 4723.

Hypotheses

Ref	Expression
aceq5lem.1	⊢ A = {u∣(u ≠ ∅ ⋀ ∃t ∈ h u = ({t} × t))}
aceq5lem.2	⊢ B = (∪A ∩ y)
aceq5lem.3	⊢ (φ ↔ ∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))

Assertion

Ref	Expression
aceq5lem5	⊢ (φ → ∃f∀w ∈ h (w ≠ ∅ → (f ‘w) ∈ w))

Distinct variable groups:   x,f,z,y,w,v,u,t,h   z,B,w,f   x,A,y,z,w

Proof of Theorem aceq5lem5

Step	Hyp	Ref	Expression
1		aceq5lem.1	. . 3 ⊢ A = {u∣(u ≠ ∅ ⋀ ∃t ∈ h u = ({t} × t))}
2		aceq5lem.2	. . 3 ⊢ B = (∪A ∩ y)
3		aceq5lem.3	. . 3 ⊢ (φ ↔ ∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
4	1, 2, 3	aceq5lem4 4721	. 2 ⊢ (φ → ∃y∀z ∈ A ∃!v v ∈ (z ∩ y))
5		pm3.27 323	. . . . . . . . . . 11 ⊢ ((w ≠ ∅ ⋀ w ∈ h) → w ∈ h)
6	5	a1i 8	. . . . . . . . . 10 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ((w ≠ ∅ ⋀ w ∈ h) → w ∈ h))
7		ineq1 2207	. . . . . . . . . . . . . 14 ⊢ (z = ({w} × w) → (z ∩ y) = (({w} × w) ∩ y))
8	7	eleq2d 1539	. . . . . . . . . . . . 13 ⊢ (z = ({w} × w) → (v ∈ (z ∩ y) ↔ v ∈ (({w} × w) ∩ y)))
9	8	eubidv 1385	. . . . . . . . . . . 12 ⊢ (z = ({w} × w) → (∃!v v ∈ (z ∩ y) ↔ ∃!v v ∈ (({w} × w) ∩ y)))
10	9	rcla4cv 1871	. . . . . . . . . . 11 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → (({w} × w) ∈ A → ∃!v v ∈ (({w} × w) ∩ y)))
11	1	aceq5lem3 4720	. . . . . . . . . . 11 ⊢ (({w} × w) ∈ A ↔ (w ≠ ∅ ⋀ w ∈ h))
12		aceq5lem1 4718	. . . . . . . . . . 11 ⊢ (∃!v v ∈ (({w} × w) ∩ y) ↔ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y))
13	10, 11, 12	3imtr3g 551	. . . . . . . . . 10 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ((w ≠ ∅ ⋀ w ∈ h) → ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
14	6, 13	jcad 599	. . . . . . . . 9 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ((w ≠ ∅ ⋀ w ∈ h) → (w ∈ h ⋀ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y))))
15	2	eleq2i 1536	. . . . . . . . . . . 12 ⊢ (⟨w, g⟩ ∈ B ↔ ⟨w, g⟩ ∈ (∪A ∩ y))
16		elin 2204	. . . . . . . . . . . 12 ⊢ (⟨w, g⟩ ∈ (∪A ∩ y) ↔ (⟨w, g⟩ ∈ ∪A ⋀ ⟨w, g⟩ ∈ y))
17	1	aceq5lem2 4719	. . . . . . . . . . . . . 14 ⊢ (⟨w, g⟩ ∈ ∪A ↔ (w ∈ h ⋀ g ∈ w))
18	17	anbi1i 481	. . . . . . . . . . . . 13 ⊢ ((⟨w, g⟩ ∈ ∪A ⋀ ⟨w, g⟩ ∈ y) ↔ ((w ∈ h ⋀ g ∈ w) ⋀ ⟨w, g⟩ ∈ y))
19		anass 439	. . . . . . . . . . . . 13 ⊢ (((w ∈ h ⋀ g ∈ w) ⋀ ⟨w, g⟩ ∈ y) ↔ (w ∈ h ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
20	18, 19	bitr 173	. . . . . . . . . . . 12 ⊢ ((⟨w, g⟩ ∈ ∪A ⋀ ⟨w, g⟩ ∈ y) ↔ (w ∈ h ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
21	15, 16, 20	3bitr 177	. . . . . . . . . . 11 ⊢ (⟨w, g⟩ ∈ B ↔ (w ∈ h ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
22	21	eubii 1386	. . . . . . . . . 10 ⊢ (∃!g⟨w, g⟩ ∈ B ↔ ∃!g(w ∈ h ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
23		euanv 1431	. . . . . . . . . 10 ⊢ (∃!g(w ∈ h ⋀ (g ∈ w ⋀ ⟨w, g⟩ ∈ y)) ↔ (w ∈ h ⋀ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y)))
24	22, 23	bitr2 174	. . . . . . . . 9 ⊢ ((w ∈ h ⋀ ∃!g(g ∈ w ⋀ ⟨w, g⟩ ∈ y)) ↔ ∃!g⟨w, g⟩ ∈ B)
25	14, 24	syl6ib 212	. . . . . . . 8 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ((w ≠ ∅ ⋀ w ∈ h) → ∃!g⟨w, g⟩ ∈ B))
26		euex 1393	. . . . . . . . 9 ⊢ (∃!g⟨w, g⟩ ∈ B → ∃g⟨w, g⟩ ∈ B)
27		hbeu1 1387	. . . . . . . . . . 11 ⊢ (∃!g⟨w, g⟩ ∈ B → ∀g∃!g⟨w, g⟩ ∈ B)
28		ax-17 970	. . . . . . . . . . 11 ⊢ ((B ‘w) ∈ w → ∀g(B ‘w) ∈ w)
29	27, 28	hbim 1006	. . . . . . . . . 10 ⊢ ((∃!g⟨w, g⟩ ∈ B → (B ‘w) ∈ w) → ∀g(∃!g⟨w, g⟩ ∈ B → (B ‘w) ∈ w))
30	21	pm3.27bi 326	. . . . . . . . . . . 12 ⊢ (⟨w, g⟩ ∈ B → (g ∈ w ⋀ ⟨w, g⟩ ∈ y))
31	30	pm3.26d 321	. . . . . . . . . . 11 ⊢ (⟨w, g⟩ ∈ B → g ∈ w)
32		visset 1810	. . . . . . . . . . . . . . 15 ⊢ w ∈ V
33	32	tz6.12 3732	. . . . . . . . . . . . . 14 ⊢ ((⟨w, g⟩ ∈ B ⋀ ∃!g⟨w, g⟩ ∈ B) → (B ‘w) = g)
34	33	eleq1d 1538	. . . . . . . . . . . . 13 ⊢ ((⟨w, g⟩ ∈ B ⋀ ∃!g⟨w, g⟩ ∈ B) → ((B ‘w) ∈ w ↔ g ∈ w))
35	34	biimparc 419	. . . . . . . . . . . 12 ⊢ ((g ∈ w ⋀ (⟨w, g⟩ ∈ B ⋀ ∃!g⟨w, g⟩ ∈ B)) → (B ‘w) ∈ w)
36	35	exp32 377	. . . . . . . . . . 11 ⊢ (g ∈ w → (⟨w, g⟩ ∈ B → (∃!g⟨w, g⟩ ∈ B → (B ‘w) ∈ w)))
37	31, 36	mpcom 49	. . . . . . . . . 10 ⊢ (⟨w, g⟩ ∈ B → (∃!g⟨w, g⟩ ∈ B → (B ‘w) ∈ w))
38	29, 37	19.23ai 1063	. . . . . . . . 9 ⊢ (∃g⟨w, g⟩ ∈ B → (∃!g⟨w, g⟩ ∈ B → (B ‘w) ∈ w))
39	26, 38	mpcom 49	. . . . . . . 8 ⊢ (∃!g⟨w, g⟩ ∈ B → (B ‘w) ∈ w)
40	25, 39	syl6 22	. . . . . . 7 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ((w ≠ ∅ ⋀ w ∈ h) → (B ‘w) ∈ w))
41	40	exp3a 375	. . . . . 6 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → (w ≠ ∅ → (w ∈ h → (B ‘w) ∈ w)))
42	41	com23 32	. . . . 5 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → (w ∈ h → (w ≠ ∅ → (B ‘w) ∈ w)))
43	42	r19.21aiv 1711	. . . 4 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ∀w ∈ h (w ≠ ∅ → (B ‘w) ∈ w))
44		visset 1810	. . . . . . 7 ⊢ y ∈ V
45	44	inex2 2713	. . . . . 6 ⊢ (∪A ∩ y) ∈ V
46	2, 45	eqeltr 1542	. . . . 5 ⊢ B ∈ V
47		fveq1 3718	. . . . . . . 8 ⊢ (f = B → (f ‘w) = (B ‘w))
48	47	eleq1d 1538	. . . . . . 7 ⊢ (f = B → ((f ‘w) ∈ w ↔ (B ‘w) ∈ w))
49	48	imbi2d 611	. . . . . 6 ⊢ (f = B → ((w ≠ ∅ → (f ‘w) ∈ w) ↔ (w ≠ ∅ → (B ‘w) ∈ w)))
50	49	ralbidv 1661	. . . . 5 ⊢ (f = B → (∀w ∈ h (w ≠ ∅ → (f ‘w) ∈ w) ↔ ∀w ∈ h (w ≠ ∅ → (B ‘w) ∈ w)))
51	46, 50	cla4ev 1866	. . . 4 ⊢ (∀w ∈ h (w ≠ ∅ → (B ‘w) ∈ w) → ∃f∀w ∈ h (w ≠ ∅ → (f ‘w) ∈ w))
52	43, 51	syl 10	. . 3 ⊢ (∀z ∈ A ∃!v v ∈ (z ∩ y) → ∃f∀w ∈ h (w ≠ ∅ → (f ‘w) ∈ w))
53	52	19.23aiv 1294	. 2 ⊢ (∃y∀z ∈ A ∃!v v ∈ (z ∩ y) → ∃f∀w ∈ h (w ≠ ∅ → (f ‘w) ∈ w))
54	4, 53	syl 10	1 ⊢ (φ → ∃f∀w ∈ h (w ≠ ∅ → (f ‘w) ∈ w))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979  ∃!weu 1379  {cab 1462   ≠ wne 1583  ∀wral 1643  ∃wrex 1644  Vcvv 1808   ∩ cin 2043  ∅c0 2277  {csn 2406  ⟨cop 2408  ∪cuni 2499   × cxp 3164   ‘cfv 3178

This theorem is referenced by:  aceq5 4723

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-rab 1650  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-id 2831  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fun 3188  df-fv 3194

Copyright terms: Public domain