Theorem fiintim 6894

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 6727	. . . . . 6 ⊢ (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦)
2		ensym 6747	. . . . . . . 8 ⊢ (𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥)
3		breq1 3985	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥))
4	3	anbi2d 460	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
5	4	imbi1d 230	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
6	5	albidv 1812	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
7		breq1 3985	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥))
8	7	anbi2d 460	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥)))
9	8	imbi1d 230	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
10	9	albidv 1812	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
11		breq1 3985	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑣 → (𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥))
12	11	anbi2d 460	. . . . . . . . . . . . . 14 ⊢ (𝑦 = suc 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥)))
13	12	imbi1d 230	. . . . . . . . . . . . 13 ⊢ (𝑦 = suc 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
14	13	albidv 1812	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
15		ensym 6747	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑥 → 𝑥 ≈ ∅)
16		en0 6761	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
17	15, 16	sylib 121	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ≈ 𝑥 → 𝑥 = ∅)
18	17	anim1i 338	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ≈ 𝑥 ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
19	18	ancoms 266	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
20	19	adantll 468	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21		df-ne 2337	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22		pm3.24 683	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
23	22	pm2.21i 636	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → ∩ 𝑥 ∈ 𝐴)
24	21, 23	sylan2b 285	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)
25	20, 24	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
26	25	ax-gen 1437	. . . . . . . . . . . . 13 ⊢ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
27	26	a1i 9	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
28		nfv 1516	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
29		nfa1 1529	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
30		simpl 108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → 𝑥 ⊆ 𝐴)
31		bren 6713	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑣 ≈ 𝑥 ↔ ∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥)
32		ssel 3136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ⊆ 𝐴 → ((𝑓‘𝑣) ∈ 𝑥 → (𝑓‘𝑣) ∈ 𝐴))
33		f1of 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣⟶𝑥)
34		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑣 ∈ V
35	34	sucid 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑣 ∈ suc 𝑣
36		ffvelrn 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:suc 𝑣⟶𝑥 ∧ 𝑣 ∈ suc 𝑣) → (𝑓‘𝑣) ∈ 𝑥)
37	33, 35, 36	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓‘𝑣) ∈ 𝑥)
38	32, 37	impel 278	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) → (𝑓‘𝑣) ∈ 𝐴)
39	38	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
40	39	adantlll 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
41		imaeq2 4942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = (𝑓 “ ∅))
42		ima0 4963	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 “ ∅) = ∅
43	41, 42	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = ∅)
44		inteq 3827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = ∩ ∅)
45		int0 3838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∩ ∅ = V
46	44, 45	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = V)
47	46	ineq1d 3322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (V ∩ (𝑓‘𝑣)))
48		ssv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓‘𝑣) ⊆ V
49		sseqin2 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓‘𝑣) ⊆ V ↔ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
50	48, 49	mpbi 144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)
51	47, 50	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
52	51	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑣) = ∅ → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ (𝑓‘𝑣) ∈ 𝐴))
53	52	biimprd 157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
55	54	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
56		f1ofun 5434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → Fun 𝑓)
57	56	ad3antlr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58		elelsuc 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
59	58	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60		f1odm 5436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → dom 𝑓 = suc 𝑣)
61	60	eleq2d 2236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
62	61	ad3antlr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
63	59, 62	mpbird 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓)
64	57, 63	jca 304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓))
65		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣)
66		funfvima 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓 “ 𝑣)))
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓 “ 𝑣))
68		ne0i 3415	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓‘∅) ∈ (𝑓 “ 𝑣) → (𝑓 “ 𝑣) ≠ ∅)
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓 “ 𝑣) ≠ ∅)
70		imassrn 4957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓 “ 𝑣) ⊆ ran 𝑓
71		dff1o2 5437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑥))
72	71	simp3bi 1004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ran 𝑓 = 𝑥)
73	70, 72	sseqtrid 3192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ⊆ 𝑥)
74		sstr2 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓 “ 𝑣) ⊆ 𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
76	75	anim1d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
77		f1of1 5431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–1-1→𝑥)
78		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 𝑥 ∈ V
79		sssucid 4393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 𝑣 ⊆ suc 𝑣
80		f1imaen2g 6759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V)) → (𝑓 “ 𝑣) ≈ 𝑣)
81	79, 34, 80	mpanr12 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑣) ≈ 𝑣)
82	77, 78, 81	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ≈ 𝑣)
83	82	ensymd 6749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑣 ≈ (𝑓 “ 𝑣))
84	76, 83	jctird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
85		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑓 ∈ V
86	85	imaex 4959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 “ 𝑣) ∈ V
87		sseq1 3165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ 𝑣) ⊆ 𝐴))
88		neeq1 2349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ≠ ∅ ↔ (𝑓 “ 𝑣) ≠ ∅))
89	87, 88	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
90		breq2 3986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑣 ≈ 𝑥 ↔ 𝑣 ≈ (𝑓 “ 𝑣)))
91	89, 90	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) ↔ (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
92		inteq 3827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → ∩ 𝑥 = ∩ (𝑓 “ 𝑣))
93	92	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (∩ 𝑥 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑣) ∈ 𝐴))
94	91, 93	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴)))
95	86, 94	spcv 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
96	84, 95	sylan9 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
97		ineq1 3316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → (𝑧 ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ 𝑤))
98	97	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴))
99		ineq2 3317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤 = (𝑓‘𝑣) → (∩ (𝑓 “ 𝑣) ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)))
100	99	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 = (𝑓‘𝑣) → ((∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
101	98, 100	rspc2v 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
106	105	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
107	106	imp43 353	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
108	107	adantlll 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
109	108	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
111		0elnn 4596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112	111	ad3antrrr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
113	55, 110, 112	mpjaodan 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)
115	85, 34	fvex 5506	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑣) ∈ V
116	115	intunsn 3862	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣))
117		f1ofn 5433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓 Fn suc 𝑣)
118		fnsnfv 5545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣) → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
119	117, 35, 118	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
120	119	uneq2d 3276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})))
121		df-suc 4349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑣 = (𝑣 ∪ {𝑣})
122	121	imaeq2i 4944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123		imaundi 5016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣}))
124	122, 123	eqtr2i 2187	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125	120, 124	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (𝑓 “ suc 𝑣))
126		f1ofo 5439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–onto→𝑥)
127		foima 5415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129	125, 128	eqtrd 2198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = 𝑥)
130	129	inteqd 3829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ∩ 𝑥)
131	116, 130	eqtr3id 2213	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = ∩ 𝑥)
132	131	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
133	132	ad2antlr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
134	114, 133	mpbid 146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ∩ 𝑥 ∈ 𝐴)
135	134	exp43 370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
136	135	exlimdv 1807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
137	31, 136	syl5bi 151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (suc 𝑣 ≈ 𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
138	137	expimpd 361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
139	30, 138	sylani 404	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ω → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
140	139	com24 87	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
141	140	imp 123	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
142	28, 29, 141	alrimd 1598	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
143	142	ex 114	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
144	6, 10, 14, 27, 143	finds2 4578	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
145		sp 1499	. . . . . . . . . . 11 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
146	144, 145	syl6 33	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
147	146	exp4a 364	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴))))
148	147	com24 87	. . . . . . . 8 ⊢ (𝑦 ∈ ω → (𝑦 ≈ 𝑥 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
149	2, 148	syl5 32	. . . . . . 7 ⊢ (𝑦 ∈ ω → (𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
150	149	rexlimiv 2577	. . . . . 6 ⊢ (∃𝑦 ∈ ω 𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
151	1, 150	sylbi 120	. . . . 5 ⊢ (𝑥 ∈ Fin → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
152	151	com13 80	. . . 4 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑥 ∈ Fin → ∩ 𝑥 ∈ 𝐴)))
153	152	impd 252	. . 3 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
154	153	alrimiv 1862	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
155		ineq1 3316	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑦) = (𝑧 ∩ 𝑦))
156	155	eleq1d 2235	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑦) ∈ 𝐴))
157		ineq2 3317	. . . 4 ⊢ (𝑦 = 𝑤 → (𝑧 ∩ 𝑦) = (𝑧 ∩ 𝑤))
158	157	eleq1d 2235	. . 3 ⊢ (𝑦 = 𝑤 → ((𝑧 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴))
159	156, 158	cbvral2v 2705	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
160		df-3an 970	. . . 4 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161	160	imbi1i 237	. . 3 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
162	161	albii 1458	. 2 ⊢ (∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
163	154, 159, 162	3imtr4i 200	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 968  ∀wal 1341   = wceq 1343  ∃wex 1480   ∈ wcel 2136   ≠ wne 2336  ∀wral 2444  ∃wrex 2445  Vcvv 2726   ∪ cun 3114   ∩ cin 3115   ⊆ wss 3116  ∅c0 3409  {csn 3576  ∩ cint 3824   class class class wbr 3982  suc csuc 4343  ωcom 4567  ^◡ccnv 4603  dom cdm 4604  ran crn 4605   “ cima 4607  Fun wfun 5182   Fn wfn 5183  ⟶wf 5184  –1-1→wf1 5185  –onto→wfo 5186  –1-1-onto→wf1o 5187  ‘cfv 5188   ≈ cen 6704  Fincfn 6706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-nul 4108  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-iinf 4565

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-ral 2449  df-rex 2450  df-v 2728  df-sbc 2952  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-br 3983  df-opab 4044  df-id 4271  df-suc 4349  df-iom 4568  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-er 6501  df-en 6707  df-fin 6709

This theorem is referenced by:  istopfin  12638