Theorem fiintim 6958

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 6788	. . . . . 6 ⊢ (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦)
2		ensym 6808	. . . . . . . 8 ⊢ (𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥)
3		breq1 4021	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥))
4	3	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
5	4	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
6	5	albidv 1835	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
7		breq1 4021	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥))
8	7	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥)))
9	8	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
10	9	albidv 1835	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
11		breq1 4021	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑣 → (𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥))
12	11	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ (𝑦 = suc 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥)))
13	12	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑦 = suc 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
14	13	albidv 1835	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
15		ensym 6808	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑥 → 𝑥 ≈ ∅)
16		en0 6822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
17	15, 16	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ≈ 𝑥 → 𝑥 = ∅)
18	17	anim1i 340	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ≈ 𝑥 ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
19	18	ancoms 268	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
20	19	adantll 476	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21		df-ne 2361	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22		pm3.24 694	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
23	22	pm2.21i 647	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → ∩ 𝑥 ∈ 𝐴)
24	21, 23	sylan2b 287	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)
25	20, 24	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
26	25	ax-gen 1460	. . . . . . . . . . . . 13 ⊢ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
27	26	a1i 9	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
28		nfv 1539	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
29		nfa1 1552	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
30		simpl 109	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → 𝑥 ⊆ 𝐴)
31		bren 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑣 ≈ 𝑥 ↔ ∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥)
32		ssel 3164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ⊆ 𝐴 → ((𝑓‘𝑣) ∈ 𝑥 → (𝑓‘𝑣) ∈ 𝐴))
33		f1of 5480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣⟶𝑥)
34		vex 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑣 ∈ V
35	34	sucid 4435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑣 ∈ suc 𝑣
36		ffvelcdm 5670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:suc 𝑣⟶𝑥 ∧ 𝑣 ∈ suc 𝑣) → (𝑓‘𝑣) ∈ 𝑥)
37	33, 35, 36	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓‘𝑣) ∈ 𝑥)
38	32, 37	impel 280	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) → (𝑓‘𝑣) ∈ 𝐴)
39	38	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
40	39	adantlll 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
41		imaeq2 4984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = (𝑓 “ ∅))
42		ima0 5005	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 “ ∅) = ∅
43	41, 42	eqtrdi 2238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = ∅)
44		inteq 3862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = ∩ ∅)
45		int0 3873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∩ ∅ = V
46	44, 45	eqtrdi 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = V)
47	46	ineq1d 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (V ∩ (𝑓‘𝑣)))
48		ssv 3192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓‘𝑣) ⊆ V
49		sseqin2 3369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓‘𝑣) ⊆ V ↔ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
50	48, 49	mpbi 145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)
51	47, 50	eqtrdi 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
52	51	eleq1d 2258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑣) = ∅ → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ (𝑓‘𝑣) ∈ 𝐴))
53	52	biimprd 158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
56		f1ofun 5482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → Fun 𝑓)
57	56	ad3antlr 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58		elelsuc 4427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
59	58	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60		f1odm 5484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → dom 𝑓 = suc 𝑣)
61	60	eleq2d 2259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
62	61	ad3antlr 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
63	59, 62	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓)
64	57, 63	jca 306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓))
65		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣)
66		funfvima 5769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓 “ 𝑣)))
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓 “ 𝑣))
68		ne0i 3444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓‘∅) ∈ (𝑓 “ 𝑣) → (𝑓 “ 𝑣) ≠ ∅)
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓 “ 𝑣) ≠ ∅)
70		imassrn 4999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓 “ 𝑣) ⊆ ran 𝑓
71		dff1o2 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑥))
72	71	simp3bi 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ran 𝑓 = 𝑥)
73	70, 72	sseqtrid 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ⊆ 𝑥)
74		sstr2 3177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓 “ 𝑣) ⊆ 𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
76	75	anim1d 336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
77		f1of1 5479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–1-1→𝑥)
78		vex 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ 𝑥 ∈ V
79		sssucid 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 𝑣 ⊆ suc 𝑣
80		f1imaen2g 6820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V)) → (𝑓 “ 𝑣) ≈ 𝑣)
81	79, 34, 80	mpanr12 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑣) ≈ 𝑣)
82	77, 78, 81	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ≈ 𝑣)
83	82	ensymd 6810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑣 ≈ (𝑓 “ 𝑣))
84	76, 83	jctird 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
85		vex 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑓 ∈ V
86	85	imaex 5001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 “ 𝑣) ∈ V
87		sseq1 3193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ 𝑣) ⊆ 𝐴))
88		neeq1 2373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ≠ ∅ ↔ (𝑓 “ 𝑣) ≠ ∅))
89	87, 88	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
90		breq2 4022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑣 ≈ 𝑥 ↔ 𝑣 ≈ (𝑓 “ 𝑣)))
91	89, 90	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) ↔ (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
92		inteq 3862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑥 = (𝑓 “ 𝑣) → ∩ 𝑥 = ∩ (𝑓 “ 𝑣))
93	92	eleq1d 2258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (∩ 𝑥 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑣) ∈ 𝐴))
94	91, 93	imbi12d 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴)))
95	86, 94	spcv 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
96	84, 95	sylan9 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
97		ineq1 3344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → (𝑧 ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ 𝑤))
98	97	eleq1d 2258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴))
99		ineq2 3345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤 = (𝑓‘𝑣) → (∩ (𝑓 “ 𝑣) ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)))
100	99	eleq1d 2258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 = (𝑓‘𝑣) → ((∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
101	98, 100	rspc2v 2869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∩ (𝑓 “ 𝑣) ∈ 𝐴 ∧ (𝑓‘𝑣) ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
102	101	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∩ (𝑓 “ 𝑣) ∈ 𝐴 → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
103	96, 102	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))
104	103	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))
105	104	exp5c 376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
106	105	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
107	106	imp43 355	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
108	107	adantlll 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
109	108	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
111		0elnn 4636	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112	111	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
113	55, 110, 112	mpjaodan 799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)
115	85, 34	fvex 5554	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑣) ∈ V
116	115	intunsn 3897	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣))
117		f1ofn 5481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓 Fn suc 𝑣)
118		fnsnfv 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣) → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
119	117, 35, 118	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
120	119	uneq2d 3304	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})))
121		df-suc 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑣 = (𝑣 ∪ {𝑣})
122	121	imaeq2i 4986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123		imaundi 5059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣}))
124	122, 123	eqtr2i 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125	120, 124	eqtrdi 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (𝑓 “ suc 𝑣))
126		f1ofo 5487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–onto→𝑥)
127		foima 5462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129	125, 128	eqtrd 2222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = 𝑥)
130	129	inteqd 3864	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ∩ 𝑥)
131	116, 130	eqtr3id 2236	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = ∩ 𝑥)
132	131	eleq1d 2258	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
133	132	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
134	114, 133	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ∩ 𝑥 ∈ 𝐴)
135	134	exp43 372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
136	135	exlimdv 1830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
137	31, 136	biimtrid 152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (suc 𝑣 ≈ 𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
138	137	expimpd 363	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
139	30, 138	sylani 406	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ω → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
140	139	com24 87	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
141	140	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
142	28, 29, 141	alrimd 1621	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
143	142	ex 115	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
144	6, 10, 14, 27, 143	finds2 4618	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
145		sp 1522	. . . . . . . . . . 11 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
146	144, 145	syl6 33	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
147	146	exp4a 366	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴))))
148	147	com24 87	. . . . . . . 8 ⊢ (𝑦 ∈ ω → (𝑦 ≈ 𝑥 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
149	2, 148	syl5 32	. . . . . . 7 ⊢ (𝑦 ∈ ω → (𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
150	149	rexlimiv 2601	. . . . . 6 ⊢ (∃𝑦 ∈ ω 𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
151	1, 150	sylbi 121	. . . . 5 ⊢ (𝑥 ∈ Fin → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
152	151	com13 80	. . . 4 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑥 ∈ Fin → ∩ 𝑥 ∈ 𝐴)))
153	152	impd 254	. . 3 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
154	153	alrimiv 1885	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
155		ineq1 3344	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑦) = (𝑧 ∩ 𝑦))
156	155	eleq1d 2258	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑦) ∈ 𝐴))
157		ineq2 3345	. . . 4 ⊢ (𝑦 = 𝑤 → (𝑧 ∩ 𝑦) = (𝑧 ∩ 𝑤))
158	157	eleq1d 2258	. . 3 ⊢ (𝑦 = 𝑤 → ((𝑧 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴))
159	156, 158	cbvral2v 2731	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
160		df-3an 982	. . . 4 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161	160	imbi1i 238	. . 3 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
162	161	albii 1481	. 2 ⊢ (∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
163	154, 159, 162	3imtr4i 201	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709   ∧ w3a 980  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2160   ≠ wne 2360  ∀wral 2468  ∃wrex 2469  Vcvv 2752   ∪ cun 3142   ∩ cin 3143   ⊆ wss 3144  ∅c0 3437  {csn 3607  ∩ cint 3859   class class class wbr 4018  suc csuc 4383  ωcom 4607  ^◡ccnv 4643  dom cdm 4644  ran crn 4645   “ cima 4647  Fun wfun 5229   Fn wfn 5230  ⟶wf 5231  –1-1→wf1 5232  –onto→wfo 5233  –1-1-onto→wf1o 5234  ‘cfv 5235   ≈ cen 6765  Fincfn 6767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-iinf 4605

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-id 4311  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-er 6560  df-en 6768  df-fin 6770

This theorem is referenced by:  istopfin  13977