Theorem fiv 10374

Description: The set of all the finite intersections of the elements of A.

Assertion

Ref	Expression
fiv	⊢ (A ∈ B → (fi ‘A) = {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})

Distinct variable groups:   u,A,z   u,a,z

Proof of Theorem fiv

Step	Hyp	Ref	Expression
1		sseq2 2073	. . . . . 6 ⊢ (x = A → (z ⊆ x ↔ z ⊆ A))
2	1	3anbi1d 894	. . . . 5 ⊢ (x = A → ((z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z) ↔ (z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)))
3	2	exbidv 1274	. . . 4 ⊢ (x = A → (∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z) ↔ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)))
4	3	abbidv 1569	. . 3 ⊢ (x = A → {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)} = {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})
5		df-fiNEW 10373	. . . 4 ⊢ fi = {⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}}
6		relopab 3256	. . . . 5 ⊢ Rel {⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}}
7		resid 3384	. . . . 5 ⊢ (Rel {⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}} → ({⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}} ↾ V) = {⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}})
8	6, 7	ax-mp 7	. . . 4 ⊢ ({⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}} ↾ V) = {⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}}
9		resopab 3379	. . . 4 ⊢ ({⟨x, y⟩∣y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}} ↾ V) = {⟨x, y⟩∣(x ∈ V ⋀ y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})}
10	5, 8, 9	3eqtr2 1493	. . 3 ⊢ fi = {⟨x, y⟩∣(x ∈ V ⋀ y = {u∣∃z(z ⊆ x ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})}
11	4, 10	fvopab4g 3764	. 2 ⊢ ((A ∈ V ⋀ {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)} ∈ V) → (fi ‘A) = {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})
12		elisset 1808	. 2 ⊢ (A ∈ B → A ∈ V)
13		uniexg 2862	. . . . . 6 ⊢ (A ∈ B → ∪A ∈ V)
14		pwexg 2736	. . . . . 6 ⊢ (∪A ∈ V → ℘∪A ∈ V)
15	13, 14	syl 10	. . . . 5 ⊢ (A ∈ B → ℘∪A ∈ V)
16		rabexg 2714	. . . . 5 ⊢ (℘∪A ∈ V → {u ∈ ℘∪A∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)} ∈ V)
17	15, 16	syl 10	. . . 4 ⊢ (A ∈ B → {u ∈ ℘∪A∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)} ∈ V)
18		df-rab 1644	. . . 4 ⊢ {u ∈ ℘∪A∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)} = {u∣(u ∈ ℘∪A ⋀ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z))}
19	17, 18	syl5eqelr 1545	. . 3 ⊢ (A ∈ B → {u∣(u ∈ ℘∪A ⋀ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z))} ∈ V)
20		pm3.27 323	. . . . 5 ⊢ ((u ∈ ℘∪A ⋀ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)) → ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z))
21		visset 1804	. . . . . . . . 9 ⊢ u ∈ V
22		eleq1 1526	. . . . . . . . . . . 12 ⊢ (u = ∩z → (u ∈ V ↔ ∩z ∈ V))
23		intex 2719	. . . . . . . . . . . . 13 ⊢ (z ≠ ∅ ↔ ∩z ∈ V)
24		intssuni2 2546	. . . . . . . . . . . . . . . 16 ⊢ ((z ⊆ A ⋀ z ≠ ∅) → ∩z ⊆ ∪A)
25	24	ex 373	. . . . . . . . . . . . . . 15 ⊢ (z ⊆ A → (z ≠ ∅ → ∩z ⊆ ∪A))
26		sseq1 2072	. . . . . . . . . . . . . . . . 17 ⊢ (u = ∩z → (u ⊆ ∪A ↔ ∩z ⊆ ∪A))
27	26	biimprd 154	. . . . . . . . . . . . . . . 16 ⊢ (u = ∩z → (∩z ⊆ ∪A → u ⊆ ∪A))
28	21	elpw 2394	. . . . . . . . . . . . . . . . . 18 ⊢ (u ∈ ℘∪A ↔ u ⊆ ∪A)
29	28	biimpr 152	. . . . . . . . . . . . . . . . 17 ⊢ (u ⊆ ∪A → u ∈ ℘∪A)
30	29	a1d 12	. . . . . . . . . . . . . . . 16 ⊢ (u ⊆ ∪A → (∃a ∈ ω z ≈ a → u ∈ ℘∪A))
31	27, 30	syl6com 53	. . . . . . . . . . . . . . 15 ⊢ (∩z ⊆ ∪A → (u = ∩z → (∃a ∈ ω z ≈ a → u ∈ ℘∪A)))
32	25, 31	syl6 22	. . . . . . . . . . . . . 14 ⊢ (z ⊆ A → (z ≠ ∅ → (u = ∩z → (∃a ∈ ω z ≈ a → u ∈ ℘∪A))))
33	32	com3l 34	. . . . . . . . . . . . 13 ⊢ (z ≠ ∅ → (u = ∩z → (z ⊆ A → (∃a ∈ ω z ≈ a → u ∈ ℘∪A))))
34	23, 33	sylbir 201	. . . . . . . . . . . 12 ⊢ (∩z ∈ V → (u = ∩z → (z ⊆ A → (∃a ∈ ω z ≈ a → u ∈ ℘∪A))))
35	22, 34	syl6bi 214	. . . . . . . . . . 11 ⊢ (u = ∩z → (u ∈ V → (u = ∩z → (z ⊆ A → (∃a ∈ ω z ≈ a → u ∈ ℘∪A)))))
36	35	pm2.43a 66	. . . . . . . . . 10 ⊢ (u = ∩z → (u ∈ V → (z ⊆ A → (∃a ∈ ω z ≈ a → u ∈ ℘∪A))))
37	36	com4l 39	. . . . . . . . 9 ⊢ (u ∈ V → (z ⊆ A → (∃a ∈ ω z ≈ a → (u = ∩z → u ∈ ℘∪A))))
38	21, 37	ax-mp 7	. . . . . . . 8 ⊢ (z ⊆ A → (∃a ∈ ω z ≈ a → (u = ∩z → u ∈ ℘∪A)))
39	38	3imp 825	. . . . . . 7 ⊢ ((z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z) → u ∈ ℘∪A)
40	39	19.23aiv 1290	. . . . . 6 ⊢ (∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z) → u ∈ ℘∪A)
41	40	ancri 297	. . . . 5 ⊢ (∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z) → (u ∈ ℘∪A ⋀ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)))
42	20, 41	impbi 157	. . . 4 ⊢ ((u ∈ ℘∪A ⋀ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)) ↔ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z))
43	42	abbii 1567	. . 3 ⊢ {u∣(u ∈ ℘∪A ⋀ ∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z))} = {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)}
44	19, 43	syl5eqelr 1545	. 2 ⊢ (A ∈ B → {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)} ∈ V)
45	11, 12, 44	sylanc 471	1 ⊢ (A ∈ B → (fi ‘A) = {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 773   = wceq 953   ∈ wcel 955  ∃wex 977  {cab 1456   ≠ wne 1577  ∃wrex 1638  {crab 1640  Vcvv 1802   ⊆ wss 2037  ∅c0 2270  ℘cpw 2391  ∪cuni 2493  ∩cint 2523   class class class wbr 2609  {copab 2656  ωcom 3121   ↾ cres 3162  Rel wrel 3165   ‘cfv 3172   ≈ cen 4348  ficfi 10372

This theorem is referenced by:  fine2 10375  sppfi 10376  abfi2 10378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-rab 1644  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-int 2524  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fv 3188  df-fiNEW 10373

Copyright terms: Public domain