Theorem aceq3lem 3555

Description: Lemma for aceq3 3556.

Hypothesis

Ref	Expression
aceq3lem.1	⊢ F = {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))}

Assertion

Ref	Expression
aceq3lem	⊢ (∀x∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃f(f ⊆ y ∧ f Fn dom y))

Distinct variable group(s):   x,y,z,w,v,u,f

Proof of Theorem aceq3lem

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 ⊢ y ∈ V
2		rnexg 2569	. . . . . 6 ⊢ (y ∈ V → ran y ∈ V)
3	1, 2	ax-mp 6	. . . . 5 ⊢ ran y ∈ V
4	3	pwex 1806	. . . 4 ⊢ ℘ran y ∈ V
5		raleq 1324	. . . . 5 ⊢ (x = ℘ran y → (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) ↔ ∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z)))
6	5	biexdv 936	. . . 4 ⊢ (x = ℘ran y → (∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) ↔ ∃f∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z)))
7	4, 6	cla4v 1400	. . 3 ⊢ (∀x∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃f∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z))
8		relopab 2494	. . . . . . . . 9 ⊢ Rel {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))}
9		aceq3lem.1	. . . . . . . . . 10 ⊢ F = {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))}
10		releq 2477	. . . . . . . . . 10 ⊢ (F = {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))} → (Rel F ↔ Rel {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))}))
11	9, 10	ax-mp 6	. . . . . . . . 9 ⊢ (Rel F ↔ Rel {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))})
12	8, 11	mpbir 165	. . . . . . . 8 ⊢ Rel F
13	12	a1i 7	. . . . . . 7 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → Rel F)
14	9	eleq2i 1153	. . . . . . . . . . . 12 ⊢ (⟨t, h⟩ ∈ F ↔ ⟨t, h⟩ ∈ {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))})
15		visset 1350	. . . . . . . . . . . . 13 ⊢ t ∈ V
16		visset 1350	. . . . . . . . . . . . 13 ⊢ h ∈ V
17		eleq1 1149	. . . . . . . . . . . . . 14 ⊢ (w = t → (w ∈ dom y ↔ t ∈ dom y))
18		breq1 2065	. . . . . . . . . . . . . . . . 17 ⊢ (w = t → (wyu ↔ tyu))
19	18	biabdv 1183	. . . . . . . . . . . . . . . 16 ⊢ (w = t → {u∣wyu} = {u∣tyu})
20	19	fveq2d 2836	. . . . . . . . . . . . . . 15 ⊢ (w = t → (f ‘{u∣wyu}) = (f ‘{u∣tyu}))
21	20	cleq2d 1112	. . . . . . . . . . . . . 14 ⊢ (w = t → (v = (f ‘{u∣wyu}) ↔ v = (f ‘{u∣tyu})))
22	17, 21	anbi12d 476	. . . . . . . . . . . . 13 ⊢ (w = t → ((w ∈ dom y ∧ v = (f ‘{u∣wyu})) ↔ (t ∈ dom y ∧ v = (f ‘{u∣tyu}))))
23		cleq1 1107	. . . . . . . . . . . . . 14 ⊢ (v = h → (v = (f ‘{u∣tyu}) ↔ h = (f ‘{u∣tyu})))
24	23	anbi2d 468	. . . . . . . . . . . . 13 ⊢ (v = h → ((t ∈ dom y ∧ v = (f ‘{u∣tyu})) ↔ (t ∈ dom y ∧ h = (f ‘{u∣tyu}))))
25	15, 16, 22, 24	opelopab 2117	. . . . . . . . . . . 12 ⊢ (⟨t, h⟩ ∈ {⟨w, v⟩∣(w ∈ dom y ∧ v = (f ‘{u∣wyu}))} ↔ (t ∈ dom y ∧ h = (f ‘{u∣tyu})))
26	14, 25	bitr 151	. . . . . . . . . . 11 ⊢ (⟨t, h⟩ ∈ F ↔ (t ∈ dom y ∧ h = (f ‘{u∣tyu})))
27	26	pm3.26bd 259	. . . . . . . . . 10 ⊢ (⟨t, h⟩ ∈ F → t ∈ dom y)
28		19.8a 712	. . . . . . . . . . . . . . . . 17 ⊢ (tyu → ∃t tyu)
29	28	ss2abi 1552	. . . . . . . . . . . . . . . 16 ⊢ {u∣tyu} ⊆ {u∣∃t tyu}
30		dfrn2 2523	. . . . . . . . . . . . . . . 16 ⊢ ran y = {u∣∃t tyu}
31	29, 30	sseqtr4 1533	. . . . . . . . . . . . . . 15 ⊢ {u∣tyu} ⊆ ran y
32		elpw2g 1803	. . . . . . . . . . . . . . . 16 ⊢ (ran y ∈ V → ({u∣tyu} ∈ ℘ran y ↔ {u∣tyu} ⊆ ran y))
33	3, 32	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ ({u∣tyu} ∈ ℘ran y ↔ {u∣tyu} ⊆ ran y)
34	31, 33	mpbir 165	. . . . . . . . . . . . . 14 ⊢ {u∣tyu} ∈ ℘ran y
35		cleq1 1107	. . . . . . . . . . . . . . . . 17 ⊢ (z = {u∣tyu} → (z = ∅ ↔ {u∣tyu} = ∅))
36	35	negbid 463	. . . . . . . . . . . . . . . 16 ⊢ (z = {u∣tyu} → (¬ z = ∅ ↔ ¬ {u∣tyu} = ∅))
37		fveq2 2832	. . . . . . . . . . . . . . . . 17 ⊢ (z = {u∣tyu} → (f ‘z) = (f ‘{u∣tyu}))
38		id 9	. . . . . . . . . . . . . . . . 17 ⊢ (z = {u∣tyu} → z = {u∣tyu})
39	37, 38	eleq12d 1157	. . . . . . . . . . . . . . . 16 ⊢ (z = {u∣tyu} → ((f ‘z) ∈ z ↔ (f ‘{u∣tyu}) ∈ {u∣tyu}))
40	36, 39	imbi12d 474	. . . . . . . . . . . . . . 15 ⊢ (z = {u∣tyu} → ((¬ z = ∅ → (f ‘z) ∈ z) ↔ (¬ {u∣tyu} = ∅ → (f ‘{u∣tyu}) ∈ {u∣tyu})))
41	40	rcla4v 1402	. . . . . . . . . . . . . 14 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → ({u∣tyu} ∈ ℘ran y → (¬ {u∣tyu} = ∅ → (f ‘{u∣tyu}) ∈ {u∣tyu})))
42	34, 41	mpi 44	. . . . . . . . . . . . 13 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → (¬ {u∣tyu} = ∅ → (f ‘{u∣tyu}) ∈ {u∣tyu}))
43	15	eldm 2527	. . . . . . . . . . . . . 14 ⊢ (t ∈ dom y ↔ ∃u tyu)
44		abn0 1715	. . . . . . . . . . . . . 14 ⊢ (¬ {u∣tyu} = ∅ ↔ ∃u tyu)
45	43, 44	bitr4 154	. . . . . . . . . . . . 13 ⊢ (t ∈ dom y ↔ ¬ {u∣tyu} = ∅)
46	42, 45	syl5ib 181	. . . . . . . . . . . 12 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → (t ∈ dom y → (f ‘{u∣tyu}) ∈ {u∣tyu}))
47	46	com12 13	. . . . . . . . . . 11 ⊢ (t ∈ dom y → (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → (f ‘{u∣tyu}) ∈ {u∣tyu}))
48		fvex 2838	. . . . . . . . . . . . . 14 ⊢ (f ‘{u∣tyu}) ∈ V
49	20, 9, 48	fvopab4 2871	. . . . . . . . . . . . 13 ⊢ (t ∈ dom y → (F ‘t) = (f ‘{u∣tyu}))
50	49	eleq1d 1155	. . . . . . . . . . . 12 ⊢ (t ∈ dom y → ((F ‘t) ∈ {u∣tyu} ↔ (f ‘{u∣tyu}) ∈ {u∣tyu}))
51		fvex 2838	. . . . . . . . . . . . . 14 ⊢ (F ‘t) ∈ V
52		breq2 2066	. . . . . . . . . . . . . 14 ⊢ (h = (F ‘t) → (tyh ↔ ty(F ‘t)))
53		breq2 2066	. . . . . . . . . . . . . . 15 ⊢ (u = h → (tyu ↔ tyh))
54	53	cbvabv 1424	. . . . . . . . . . . . . 14 ⊢ {u∣tyu} = {h∣tyh}
55	51, 52, 54	elab2 1419	. . . . . . . . . . . . 13 ⊢ ((F ‘t) ∈ {u∣tyu} ↔ ty(F ‘t))
56		df-br 2063	. . . . . . . . . . . . 13 ⊢ (ty(F ‘t) ↔ ⟨t, (F ‘t)⟩ ∈ y)
57	55, 56	bitr2 152	. . . . . . . . . . . 12 ⊢ (⟨t, (F ‘t)⟩ ∈ y ↔ (F ‘t) ∈ {u∣tyu})
58	50, 57	syl5bb 410	. . . . . . . . . . 11 ⊢ (t ∈ dom y → (⟨t, (F ‘t)⟩ ∈ y ↔ (f ‘{u∣tyu}) ∈ {u∣tyu}))
59	47, 58	sylibrd 179	. . . . . . . . . 10 ⊢ (t ∈ dom y → (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → ⟨t, (F ‘t)⟩ ∈ y))
60	27, 59	syl 12	. . . . . . . . 9 ⊢ (⟨t, h⟩ ∈ F → (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → ⟨t, (F ‘t)⟩ ∈ y))
61		fvex 2838	. . . . . . . . . . . . 13 ⊢ (f ‘{u∣wyu}) ∈ V
62	61, 9	fnopab2 2747	. . . . . . . . . . . 12 ⊢ F Fn dom y
63		fnfun 2721	. . . . . . . . . . . 12 ⊢ (F Fn dom y → Fun F)
64	62, 63	ax-mp 6	. . . . . . . . . . 11 ⊢ Fun F
65	16	funfvopi 2853	. . . . . . . . . . 11 ⊢ (Fun F → (⟨t, h⟩ ∈ F → (F ‘t) = h))
66	64, 65	ax-mp 6	. . . . . . . . . 10 ⊢ (⟨t, h⟩ ∈ F → (F ‘t) = h)
67		opeq2 1877	. . . . . . . . . . 11 ⊢ ((F ‘t) = h → ⟨t, (F ‘t)⟩ = ⟨t, h⟩)
68	67	eleq1d 1155	. . . . . . . . . 10 ⊢ ((F ‘t) = h → (⟨t, (F ‘t)⟩ ∈ y ↔ ⟨t, h⟩ ∈ y))
69	66, 68	syl 12	. . . . . . . . 9 ⊢ (⟨t, h⟩ ∈ F → (⟨t, (F ‘t)⟩ ∈ y ↔ ⟨t, h⟩ ∈ y))
70	60, 69	sylibd 177	. . . . . . . 8 ⊢ (⟨t, h⟩ ∈ F → (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → ⟨t, h⟩ ∈ y))
71	70	com12 13	. . . . . . 7 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → (⟨t, h⟩ ∈ F → ⟨t, h⟩ ∈ y))
72	13, 71	relssdv 2482	. . . . . 6 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → F ⊆ y)
73	72, 62	jctir 241	. . . . 5 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → (F ⊆ y ∧ F Fn dom y))
74		dmexg 2551	. . . . . . . 8 ⊢ (y ∈ V → dom y ∈ V)
75	1, 74	ax-mp 6	. . . . . . 7 ⊢ dom y ∈ V
76		fnex 2740	. . . . . . 7 ⊢ (dom y ∈ V → (F Fn dom y → F ∈ V))
77	75, 62, 76	mp2 43	. . . . . 6 ⊢ F ∈ V
78		sseq1 1521	. . . . . . 7 ⊢ (g = F → (g ⊆ y ↔ F ⊆ y))
79		fneq1 2718	. . . . . . 7 ⊢ (g = F → (g Fn dom y ↔ F Fn dom y))
80	78, 79	anbi12d 476	. . . . . 6 ⊢ (g = F → ((g ⊆ y ∧ g Fn dom y) ↔ (F ⊆ y ∧ F Fn dom y)))
81	77, 80	cla4ev 1401	. . . . 5 ⊢ ((F ⊆ y ∧ F Fn dom y) → ∃g(g ⊆ y ∧ g Fn dom y))
82	73, 81	syl 12	. . . 4 ⊢ (∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → ∃g(g ⊆ y ∧ g Fn dom y))
83	82	19.23aiv 952	. . 3 ⊢ (∃f∀z ∈ ℘ ran y(¬ z = ∅ → (f ‘z) ∈ z) → ∃g(g ⊆ y ∧ g Fn dom y))
84	7, 83	syl 12	. 2 ⊢ (∀x∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃g(g ⊆ y ∧ g Fn dom y))
85		sseq1 1521	. . . 4 ⊢ (g = f → (g ⊆ y ↔ f ⊆ y))
86		fneq1 2718	. . . 4 ⊢ (g = f → (g Fn dom y ↔ f Fn dom y))
87	85, 86	anbi12d 476	. . 3 ⊢ (g = f → ((g ⊆ y ∧ g Fn dom y) ↔ (f ⊆ y ∧ f Fn dom y)))
88	87	cbvexv 973	. 2 ⊢ (∃g(g ⊆ y ∧ g Fn dom y) ↔ ∃f(f ⊆ y ∧ f Fn dom y))
89	84, 88	sylib 173	1 ⊢ (∀x∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃f(f ⊆ y ∧ f Fn dom y))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ℘cpw 1798  ⟨cop 1810   class class class wbr 2054  {copab 2055  dom cdm 2410  ran crn 2411  Rel wrel 2415  Fun wfun 2416   Fn wfn 2417   ‘cfv 2422

This theorem is referenced by:  aceq3 3556

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438

metamath.org