Theorem fiintim 6693

Description: If a class is closed under pairwise intersections, then it is closed under nonempty finite intersections. The converse would appear to require an additional condition, such as 𝑥 and 𝑦 not being equal, or 𝐴 having decidable equality.

This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.)

Assertion

Ref	Expression
fiintim	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))

Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem fiintim

Dummy variables 𝑧 𝑤 𝑣 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 6532	. . . . . 6 ⊢ (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦)
2		ensym 6552	. . . . . . . 8 ⊢ (𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥)
3		breq1 3854	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥))
4	3	anbi2d 453	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
5	4	imbi1d 230	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
6	5	albidv 1753	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
7		breq1 3854	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥))
8	7	anbi2d 453	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥)))
9	8	imbi1d 230	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
10	9	albidv 1753	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
11		breq1 3854	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑣 → (𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥))
12	11	anbi2d 453	. . . . . . . . . . . . . 14 ⊢ (𝑦 = suc 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥)))
13	12	imbi1d 230	. . . . . . . . . . . . 13 ⊢ (𝑦 = suc 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
14	13	albidv 1753	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
15		ensym 6552	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑥 → 𝑥 ≈ ∅)
16		en0 6566	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
17	15, 16	sylib 121	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ≈ 𝑥 → 𝑥 = ∅)
18	17	anim1i 334	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ≈ 𝑥 ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
19	18	ancoms 265	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
20	19	adantll 461	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21		df-ne 2257	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22		pm3.24 663	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
23	22	pm2.21i 611	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → ∩ 𝑥 ∈ 𝐴)
24	21, 23	sylan2b 282	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)
25	20, 24	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
26	25	ax-gen 1384	. . . . . . . . . . . . 13 ⊢ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
27	26	a1i 9	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
28		nfv 1467	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
29		nfa1 1480	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
30		simpl 108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → 𝑥 ⊆ 𝐴)
31		bren 6518	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑣 ≈ 𝑥 ↔ ∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥)
32		ssel 3020	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ⊆ 𝐴 → ((𝑓‘𝑣) ∈ 𝑥 → (𝑓‘𝑣) ∈ 𝐴))
33		f1of 5266	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣⟶𝑥)
34		vex 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑣 ∈ V
35	34	sucid 4253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑣 ∈ suc 𝑣
36		ffvelrn 5446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:suc 𝑣⟶𝑥 ∧ 𝑣 ∈ suc 𝑣) → (𝑓‘𝑣) ∈ 𝑥)
37	33, 35, 36	sylancl 405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓‘𝑣) ∈ 𝑥)
38	32, 37	impel 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) → (𝑓‘𝑣) ∈ 𝐴)
39	38	adantr 271	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
40	39	adantlll 465	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
41		imaeq2 4783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = (𝑓 “ ∅))
42		ima0 4804	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 “ ∅) = ∅
43	41, 42	syl6eq 2137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = ∅)
44		inteq 3697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = ∩ ∅)
45		int0 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∩ ∅ = V
46	44, 45	syl6eq 2137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = V)
47	46	ineq1d 3201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (V ∩ (𝑓‘𝑣)))
48		ssv 3047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓‘𝑣) ⊆ V
49		sseqin2 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓‘𝑣) ⊆ V ↔ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
50	48, 49	mpbi 144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)
51	47, 50	syl6eq 2137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
52	51	eleq1d 2157	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑣) = ∅ → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ (𝑓‘𝑣) ∈ 𝐴))
53	52	biimprd 157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
55	54	adantl 272	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
56		f1ofun 5268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → Fun 𝑓)
57	56	ad3antlr 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58		elelsuc 4245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
59	58	adantl 272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60		f1odm 5270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → dom 𝑓 = suc 𝑣)
61	60	eleq2d 2158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
62	61	ad3antlr 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
63	59, 62	mpbird 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓)
64	57, 63	jca 301	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓))
65		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣)
66		funfvima 5540	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓 “ 𝑣)))
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓 “ 𝑣))
68		ne0i 3293	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓‘∅) ∈ (𝑓 “ 𝑣) → (𝑓 “ 𝑣) ≠ ∅)
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓 “ 𝑣) ≠ ∅)
70		imassrn 4798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓 “ 𝑣) ⊆ ran 𝑓
71		dff1o2 5271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑥))
72	71	simp3bi 961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ran 𝑓 = 𝑥)
73	70, 72	syl5sseq 3075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ⊆ 𝑥)
74		sstr2 3033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓 “ 𝑣) ⊆ 𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
76	75	anim1d 330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
77		f1of1 5265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–1-1→𝑥)
78		vex 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 𝑥 ∈ V
79		sssucid 4251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 𝑣 ⊆ suc 𝑣
80		f1imaen2g 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V)) → (𝑓 “ 𝑣) ≈ 𝑣)
81	79, 34, 80	mpanr12 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑣) ≈ 𝑣)
82	77, 78, 81	sylancl 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ≈ 𝑣)
83	82	ensymd 6554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑣 ≈ (𝑓 “ 𝑣))
84	76, 83	jctird 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
85		vex 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑓 ∈ V
86	85	imaex 4800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 “ 𝑣) ∈ V
87		sseq1 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ 𝑣) ⊆ 𝐴))
88		neeq1 2269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ≠ ∅ ↔ (𝑓 “ 𝑣) ≠ ∅))
89	87, 88	anbi12d 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
90		breq2 3855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑣 ≈ 𝑥 ↔ 𝑣 ≈ (𝑓 “ 𝑣)))
91	89, 90	anbi12d 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) ↔ (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
92		inteq 3697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → ∩ 𝑥 = ∩ (𝑓 “ 𝑣))
93	92	eleq1d 2157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (∩ 𝑥 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑣) ∈ 𝐴))
94	91, 93	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴)))
95	86, 94	spcv 2713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
96	84, 95	sylan9 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
97		ineq1 3195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → (𝑧 ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ 𝑤))
98	97	eleq1d 2157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴))
99		ineq2 3196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤 = (𝑓‘𝑣) → (∩ (𝑓 “ 𝑣) ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)))
100	99	eleq1d 2157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 = (𝑓‘𝑣) → ((∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
101	98, 100	rspc2v 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∩ (𝑓 “ 𝑣) ∈ 𝐴 ∧ (𝑓‘𝑣) ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
102	101	ex 114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∩ (𝑓 “ 𝑣) ∈ 𝐴 → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
103	96, 102	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))
104	103	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))
105	104	exp5c 369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
106	105	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
107	106	imp43 348	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
108	107	adantlll 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
109	108	adantr 271	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
111		0elnn 4445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112	111	ad3antrrr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
113	55, 110, 112	mpjaodan 748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)
115	85, 34	fvex 5338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑣) ∈ V
116	115	intunsn 3732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣))
117		f1ofn 5267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓 Fn suc 𝑣)
118		fnsnfv 5376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣) → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
119	117, 35, 118	sylancl 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
120	119	uneq2d 3155	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})))
121		df-suc 4207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑣 = (𝑣 ∪ {𝑣})
122	121	imaeq2i 4785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123		imaundi 4857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣}))
124	122, 123	eqtr2i 2110	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125	120, 124	syl6eq 2137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (𝑓 “ suc 𝑣))
126		f1ofo 5273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–onto→𝑥)
127		foima 5251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129	125, 128	eqtrd 2121	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = 𝑥)
130	129	inteqd 3699	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ∩ 𝑥)
131	116, 130	syl5eqr 2135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = ∩ 𝑥)
132	131	eleq1d 2157	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
133	132	ad2antlr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
134	114, 133	mpbid 146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ∩ 𝑥 ∈ 𝐴)
135	134	exp43 365	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
136	135	exlimdv 1748	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
137	31, 136	syl5bi 151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (suc 𝑣 ≈ 𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
138	137	expimpd 356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
139	30, 138	sylani 399	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ω → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
140	139	com24 87	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
141	140	imp 123	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
142	28, 29, 141	alrimd 1547	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
143	142	ex 114	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
144	6, 10, 14, 27, 143	finds2 4429	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
145		sp 1447	. . . . . . . . . . 11 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
146	144, 145	syl6 33	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
147	146	exp4a 359	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴))))
148	147	com24 87	. . . . . . . 8 ⊢ (𝑦 ∈ ω → (𝑦 ≈ 𝑥 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
149	2, 148	syl5 32	. . . . . . 7 ⊢ (𝑦 ∈ ω → (𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
150	149	rexlimiv 2484	. . . . . 6 ⊢ (∃𝑦 ∈ ω 𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
151	1, 150	sylbi 120	. . . . 5 ⊢ (𝑥 ∈ Fin → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
152	151	com13 80	. . . 4 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑥 ∈ Fin → ∩ 𝑥 ∈ 𝐴)))
153	152	impd 252	. . 3 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
154	153	alrimiv 1803	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
155		ineq1 3195	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑦) = (𝑧 ∩ 𝑦))
156	155	eleq1d 2157	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑦) ∈ 𝐴))
157		ineq2 3196	. . . 4 ⊢ (𝑦 = 𝑤 → (𝑧 ∩ 𝑦) = (𝑧 ∩ 𝑤))
158	157	eleq1d 2157	. . 3 ⊢ (𝑦 = 𝑤 → ((𝑧 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴))
159	156, 158	cbvral2v 2599	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
160		df-3an 927	. . . 4 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161	160	imbi1i 237	. . 3 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
162	161	albii 1405	. 2 ⊢ (∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
163	154, 159, 162	3imtr4i 200	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 665   ∧ w3a 925  ∀wal 1288   = wceq 1290  ∃wex 1427   ∈ wcel 1439   ≠ wne 2256  ∀wral 2360  ∃wrex 2361  Vcvv 2620   ∪ cun 2998   ∩ cin 2999   ⊆ wss 3000  ∅c0 3287  {csn 3450  ∩ cint 3694   class class class wbr 3851  suc csuc 4201  ωcom 4418  ^◡ccnv 4451  dom cdm 4452  ran crn 4453   “ cima 4455  Fun wfun 5022   Fn wfn 5023  ⟶wf 5024  –1-1→wf1 5025  –onto→wfo 5026  –1-1-onto→wf1o 5027  ‘cfv 5028   ≈ cen 6509  Fincfn 6511

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-nul 3971  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-iinf 4416

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-v 2622  df-sbc 2842  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-br 3852  df-opab 3906  df-id 4129  df-suc 4207  df-iom 4419  df-xp 4458  df-rel 4459  df-cnv 4460  df-co 4461  df-dm 4462  df-rn 4463  df-res 4464  df-ima 4465  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-er 6306  df-en 6512  df-fin 6514

This theorem is referenced by:  istopfin  11760