Theorem dffi2 8562

Description: The set of finite intersections is the smallest set that contains 𝐴 and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)

Assertion

Ref	Expression
dffi2	⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)})

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑦,𝑉,𝑧

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem dffi2

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3402	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		vex 3390	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
3		elfi 8552	. . . . . . . . . 10 ⊢ ((𝑡 ∈ V ∧ 𝐴 ∈ V) → (𝑡 ∈ (fi‘𝐴) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥))
4	2, 3	mpan 673	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (𝑡 ∈ (fi‘𝐴) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥))
5	4	biimpd 220	. . . . . . . 8 ⊢ (𝐴 ∈ V → (𝑡 ∈ (fi‘𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥))
6		df-rex 3098	. . . . . . . . 9 ⊢ (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥 ↔ ∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥))
7		fiint 8470	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝑧))
8		inss1 4023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
9	8	sseli 3788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴)
10	9	elpwid 4357	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴)
11	10	3ad2ant2 1157	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ⊆ 𝐴)
12		simp1 1159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝐴 ⊆ 𝑧)
13	11, 12	sstrd 3802	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ⊆ 𝑧)
14		eqvisset 3401	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = ∩ 𝑥 → ∩ 𝑥 ∈ V)
15		intex 5006	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥 ∈ V)
16	14, 15	sylibr 225	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = ∩ 𝑥 → 𝑥 ≠ ∅)
17	16	3ad2ant3 1158	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ≠ ∅)
18		inss2 4024	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ Fin
19	18	sseli 3788	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin)
20	19	3ad2ant2 1157	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ∈ Fin)
21	13, 17, 20	3jca 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin))
22	21	3expib 1145	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin)))
23		pm2.27 42	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝑧) → ∩ 𝑥 ∈ 𝑧))
24	22, 23	syl6 35	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝑧) → ∩ 𝑥 ∈ 𝑧)))
25		eleq1 2869	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = ∩ 𝑥 → (𝑡 ∈ 𝑧 ↔ ∩ 𝑥 ∈ 𝑧))
26	25	biimprd 239	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = ∩ 𝑥 → (∩ 𝑥 ∈ 𝑧 → 𝑡 ∈ 𝑧))
27	26	adantl 469	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (∩ 𝑥 ∈ 𝑧 → 𝑡 ∈ 𝑧))
28	27	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (∩ 𝑥 ∈ 𝑧 → 𝑡 ∈ 𝑧)))
29	24, 28	syldd 72	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝑧) → 𝑡 ∈ 𝑧)))
30	29	com23 86	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑧 → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝑧) → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧)))
31	30	alimdv 2007	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝑧 → (∀𝑥((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝑧) → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧)))
32	7, 31	syl5bi 233	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑧 → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧)))
33	32	imp 395	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧))
34		19.23v 2033	. . . . . . . . . 10 ⊢ (∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧) ↔ (∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧))
35	33, 34	sylib 209	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧))
36	6, 35	syl5bi 233	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥 → 𝑡 ∈ 𝑧))
37	5, 36	sylan9 499	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)) → (𝑡 ∈ (fi‘𝐴) → 𝑡 ∈ 𝑧))
38	37	ssrdv 3798	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)) → (fi‘𝐴) ⊆ 𝑧)
39	38	ex 399	. . . . 5 ⊢ (𝐴 ∈ V → ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧))
40	39	alrimiv 2017	. . . 4 ⊢ (𝐴 ∈ V → ∀𝑧((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧))
41		ssintab 4679	. . . 4 ⊢ ((fi‘𝐴) ⊆ ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ↔ ∀𝑧((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧))
42	40, 41	sylibr 225	. . 3 ⊢ (𝐴 ∈ V → (fi‘𝐴) ⊆ ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)})
43		ssfii 8558	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ⊆ (fi‘𝐴))
44		fiin 8561	. . . . . . 7 ⊢ ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → (𝑥 ∩ 𝑦) ∈ (fi‘𝐴))
45	44	rgen2a 3161	. . . . . 6 ⊢ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴)
46	45	a1i 11	. . . . 5 ⊢ (𝐴 ∈ V → ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴))
47		fvex 6415	. . . . . 6 ⊢ (fi‘𝐴) ∈ V
48		sseq2 3818	. . . . . . 7 ⊢ (𝑧 = (fi‘𝐴) → (𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ (fi‘𝐴)))
49		eleq2 2870	. . . . . . . . 9 ⊢ (𝑧 = (fi‘𝐴) → ((𝑥 ∩ 𝑦) ∈ 𝑧 ↔ (𝑥 ∩ 𝑦) ∈ (fi‘𝐴)))
50	49	raleqbi1dv 3331	. . . . . . . 8 ⊢ (𝑧 = (fi‘𝐴) → (∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴)))
51	50	raleqbi1dv 3331	. . . . . . 7 ⊢ (𝑧 = (fi‘𝐴) → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴)))
52	48, 51	anbi12d 618	. . . . . 6 ⊢ (𝑧 = (fi‘𝐴) → ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) ↔ (𝐴 ⊆ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴))))
53	47, 52	elab 3541	. . . . 5 ⊢ ((fi‘𝐴) ∈ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ↔ (𝐴 ⊆ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴)))
54	43, 46, 53	sylanbrc 574	. . . 4 ⊢ (𝐴 ∈ V → (fi‘𝐴) ∈ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)})
55		intss1 4677	. . . 4 ⊢ ((fi‘𝐴) ∈ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} → ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ⊆ (fi‘𝐴))
56	54, 55	syl 17	. . 3 ⊢ (𝐴 ∈ V → ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ⊆ (fi‘𝐴))
57	42, 56	eqssd 3809	. 2 ⊢ (𝐴 ∈ V → (fi‘𝐴) = ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)})
58	1, 57	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)})

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1100  ∀wal 1635   = wceq 1637  ∃wex 1859   ∈ wcel 2155  {cab 2788   ≠ wne 2974  ∀wral 3092  ∃wrex 3093  Vcvv 3387   ∩ cin 3762   ⊆ wss 3763  ∅c0 4110  𝒫 cpw 4345  ∩ cint 4662  ‘cfv 6095  Fincfn 8186  ficfi 8549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-oadd 7794  df-er 7973  df-en 8187  df-fin 8190  df-fi 8550

This theorem is referenced by:  fiss  8563  inficl  8564  dffi3  8570  fbssfi  21848