Theorem fiint 9231

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of 𝐴 is in 𝐴". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.) Use a separate setvar for the right-hand side and avoid ax-pow 5311. (Revised by BTernaryTau, 14-Jan-2025.)

Assertion

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

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

Proof of Theorem fiint

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

Step	Hyp	Ref	Expression
1		isfi 8916	. . . . . . 7 ⊢ (𝑧 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑧 ≈ 𝑤)
2		nnfi 9096	. . . . . . . . . 10 ⊢ (𝑤 ∈ ω → 𝑤 ∈ Fin)
3		ensymfib 9112	. . . . . . . . . 10 ⊢ (𝑤 ∈ Fin → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
5		breq1 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ 𝑧 ↔ ∅ ≈ 𝑧))
6	5	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧)))
7	6	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
8	7	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
9		breq1 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑡 → (𝑤 ≈ 𝑧 ↔ 𝑡 ≈ 𝑧))
10	9	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧)))
11	10	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
12	11	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
13		breq1 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = suc 𝑡 → (𝑤 ≈ 𝑧 ↔ suc 𝑡 ≈ 𝑧))
14	13	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = suc 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧)))
15	14	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = suc 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
16	15	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑤 = suc 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
17		en0r 8961	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ≈ 𝑧 ↔ 𝑧 = ∅)
18	17	biimpi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑧 → 𝑧 = ∅)
19	18	anim1i 616	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ≈ 𝑧 ∧ 𝑧 ≠ ∅) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
20	19	ancoms 458	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ≠ ∅ ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
21	20	adantll 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
22		df-ne 2934	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ ↔ ¬ 𝑧 = ∅)
23		pm3.24 402	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (𝑧 = ∅ ∧ ¬ 𝑧 = ∅)
24	23	pm2.21i 119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ∅ ∧ ¬ 𝑧 = ∅) → ∩ 𝑧 ∈ 𝐴)
25	22, 24	sylan2b 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = ∅ ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ 𝐴)
26	21, 25	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
27	26	ax-gen 1797	. . . . . . . . . . . . . 14 ⊢ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
28	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))
29		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴
30		nfa1 2157	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
31		bren 8897	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑡 ≈ 𝑧 ↔ ∃𝑓 𝑓:suc 𝑡–1-1-onto→𝑧)
32		ssel 3928	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ⊆ 𝐴 → ((𝑓‘𝑡) ∈ 𝑧 → (𝑓‘𝑡) ∈ 𝐴))
33		f1of 6775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡⟶𝑧)
34		vex 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑡 ∈ V
35	34	sucid 6402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑡 ∈ suc 𝑡
36		ffvelcdm 7028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:suc 𝑡⟶𝑧 ∧ 𝑡 ∈ suc 𝑡) → (𝑓‘𝑡) ∈ 𝑧)
37	33, 35, 36	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓‘𝑡) ∈ 𝑧)
38	32, 37	impel 505	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) → (𝑓‘𝑡) ∈ 𝐴)
39	38	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → (𝑓‘𝑡) ∈ 𝐴)
40		df-ne 2934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 “ 𝑡) ≠ ∅ ↔ ¬ (𝑓 “ 𝑡) = ∅)
41		imassrn 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 “ 𝑡) ⊆ ran 𝑓
42		dff1o2 6780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 ↔ (𝑓 Fn suc 𝑡 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑧))
43	42	simp3bi 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ran 𝑓 = 𝑧)
44	41, 43	sseqtrid 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓 “ 𝑡) ⊆ 𝑧)
45		sstr2 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓 “ 𝑡) ⊆ 𝑧 → (𝑧 ⊆ 𝐴 → (𝑓 “ 𝑡) ⊆ 𝐴))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑧 ⊆ 𝐴 → (𝑓 “ 𝑡) ⊆ 𝐴))
47	46	anim1d 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
48		f1of1 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡–1-1→𝑧)
49		sssucid 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑡 ⊆ suc 𝑡
50		vex 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
51		f1imaen3g 8957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓:suc 𝑡–1-1→𝑧 ∧ 𝑡 ⊆ suc 𝑡 ∧ 𝑓 ∈ V) → 𝑡 ≈ (𝑓 “ 𝑡))
52	49, 50, 51	mp3an23 1456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1→𝑧 → 𝑡 ≈ (𝑓 “ 𝑡))
53	48, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑡 ≈ (𝑓 “ 𝑡))
54	47, 53	jctird 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → (((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡))))
55	50	imaex 7858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 “ 𝑡) ∈ V
56		sseq1 3960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ⊆ 𝐴 ↔ (𝑓 “ 𝑡) ⊆ 𝐴))
57		neeq1 2995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ≠ ∅ ↔ (𝑓 “ 𝑡) ≠ ∅))
58	56, 57	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
59		breq2 5103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑡 ≈ 𝑧 ↔ 𝑡 ≈ (𝑓 “ 𝑡)))
60	58, 59	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) ↔ (((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡))))
61		inteq 4906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ∩ 𝑧 = ∩ (𝑓 “ 𝑡))
62	61	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (∩ 𝑧 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑡) ∈ 𝐴))
63	60, 62	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴)))
64	55, 63	spcv 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
65	54, 64	sylan9 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓:suc 𝑡–1-1-onto→𝑧 ∧ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)) → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
66		ineq1 4166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → (𝑣 ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ 𝑢))
67	66	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → ((𝑣 ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴))
68		ineq2 4167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 = (𝑓‘𝑡) → (∩ (𝑓 “ 𝑡) ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)))
69	68	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 = (𝑓‘𝑡) → ((∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
70	67, 69	rspc2v 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∩ (𝑓 “ 𝑡) ∈ 𝐴 ∧ (𝑓‘𝑡) ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
71	70	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∩ (𝑓 “ 𝑡) ∈ 𝐴 → ((𝑓‘𝑡) ∈ 𝐴 → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴)))
72	65, 71	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓:suc 𝑡–1-1-onto→𝑧 ∧ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)) → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ((𝑓‘𝑡) ∈ 𝐴 → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))))
73	72	com4r 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ((𝑓:suc 𝑡–1-1-onto→𝑧 ∧ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)) → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))))
74	73	exp5c 444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (𝑓:suc 𝑡–1-1-onto→𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (𝑧 ⊆ 𝐴 → ((𝑓 “ 𝑡) ≠ ∅ → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))))))
75	74	com14 96	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ⊆ 𝐴 → (𝑓:suc 𝑡–1-1-onto→𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ((𝑓 “ 𝑡) ≠ ∅ → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))))))
76	75	imp43 427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → ((𝑓 “ 𝑡) ≠ ∅ → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴)))
77	40, 76	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → (¬ (𝑓 “ 𝑡) = ∅ → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴)))
78		inteq 4906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = ∩ ∅)
79		int0 4918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∩ ∅ = V
80	78, 79	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = V)
81	80	ineq1d 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (V ∩ (𝑓‘𝑡)))
82		ssv 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑡) ⊆ V
83		sseqin2 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓‘𝑡) ⊆ V ↔ (V ∩ (𝑓‘𝑡)) = (𝑓‘𝑡))
84	82, 83	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (V ∩ (𝑓‘𝑡)) = (𝑓‘𝑡)
85	81, 84	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (𝑓‘𝑡))
86	85	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 “ 𝑡) = ∅ → ((∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴 ↔ (𝑓‘𝑡) ∈ 𝐴))
87	86	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 “ 𝑡) = ∅ → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
88	77, 87	pm2.61d2 181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → ((𝑓‘𝑡) ∈ 𝐴 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
89	39, 88	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴)
90		fvex 6848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑡) ∈ V
91	90	intunsn 4943	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡))
92		f1ofn 6776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓 Fn suc 𝑡)
93		fnsnfv 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑡 ∧ 𝑡 ∈ suc 𝑡) → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
94	92, 35, 93	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
95	94	uneq2d 4121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})))
96		df-suc 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑡 = (𝑡 ∪ {𝑡})
97	96	imaeq2i 6018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑡) = (𝑓 “ (𝑡 ∪ {𝑡}))
98		imaundi 6108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑡 ∪ {𝑡})) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡}))
99	97, 98	eqtr2i 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})) = (𝑓 “ suc 𝑡)
100	95, 99	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (𝑓 “ suc 𝑡))
101		f1ofo 6782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡–onto→𝑧)
102		foima 6752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–onto→𝑧 → (𝑓 “ suc 𝑡) = 𝑧)
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓 “ suc 𝑡) = 𝑧)
104	100, 103	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = 𝑧)
105	104	inteqd 4908	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ∩ 𝑧)
106	91, 105	eqtr3id 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = ∩ 𝑧)
107	106	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴 ↔ ∩ 𝑧 ∈ 𝐴))
108	107	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → ((∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴 ↔ ∩ 𝑧 ∈ 𝐴))
109	89, 108	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑓:suc 𝑡–1-1-onto→𝑧) ∧ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ∧ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)) → ∩ 𝑧 ∈ 𝐴)
110	109	exp43 436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ⊆ 𝐴 → (𝑓:suc 𝑡–1-1-onto→𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
111	110	exlimdv 1935	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ⊆ 𝐴 → (∃𝑓 𝑓:suc 𝑡–1-1-onto→𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
112	31, 111	biimtrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ 𝐴 → (suc 𝑡 ≈ 𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
113	112	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ⊆ 𝐴 ∧ suc 𝑡 ≈ 𝑧) → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
114	113	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
115	114	com13 88	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
116	29, 30, 115	alrimd 2223	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
117	116	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))))
118	8, 12, 16, 28, 117	finds2 7842	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
119		sp 2191	. . . . . . . . . . . 12 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))
120	118, 119	syl6 35	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
121	120	exp4a 431	. . . . . . . . . 10 ⊢ (𝑤 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (𝑤 ≈ 𝑧 → ∩ 𝑧 ∈ 𝐴))))
122	121	com24 95	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → (𝑤 ≈ 𝑧 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
123	4, 122	sylbird 260	. . . . . . . 8 ⊢ (𝑤 ∈ ω → (𝑧 ≈ 𝑤 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
124	123	rexlimiv 3131	. . . . . . 7 ⊢ (∃𝑤 ∈ ω 𝑧 ≈ 𝑤 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
125	1, 124	sylbi 217	. . . . . 6 ⊢ (𝑧 ∈ Fin → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
126	125	com13 88	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (𝑧 ∈ Fin → ∩ 𝑧 ∈ 𝐴)))
127	126	impd 410	. . . 4 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
128	127	alrimiv 1929	. . 3 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
129		zfpair2 5379	. . . . . 6 ⊢ {𝑣, 𝑢} ∈ V
130		sseq1 3960	. . . . . . . . 9 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ⊆ 𝐴 ↔ {𝑣, 𝑢} ⊆ 𝐴))
131		neeq1 2995	. . . . . . . . 9 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ≠ ∅ ↔ {𝑣, 𝑢} ≠ ∅))
132	130, 131	anbi12d 633	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅)))
133		eleq1 2825	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ∈ Fin ↔ {𝑣, 𝑢} ∈ Fin))
134	132, 133	anbi12d 633	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin)))
135		inteq 4906	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ∩ 𝑧 = ∩ {𝑣, 𝑢})
136	135	eleq1d 2822	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (∩ 𝑧 ∈ 𝐴 ↔ ∩ {𝑣, 𝑢} ∈ 𝐴))
137	134, 136	imbi12d 344	. . . . . 6 ⊢ (𝑧 = {𝑣, 𝑢} → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴)))
138	129, 137	spcv 3560	. . . . 5 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴))
139		vex 3445	. . . . . . 7 ⊢ 𝑣 ∈ V
140		vex 3445	. . . . . . 7 ⊢ 𝑢 ∈ V
141	139, 140	prss 4777	. . . . . 6 ⊢ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ↔ {𝑣, 𝑢} ⊆ 𝐴)
142	139	prnz 4735	. . . . . . 7 ⊢ {𝑣, 𝑢} ≠ ∅
143	142	biantru 529	. . . . . 6 ⊢ ({𝑣, 𝑢} ⊆ 𝐴 ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅))
144		prfi 9228	. . . . . . 7 ⊢ {𝑣, 𝑢} ∈ Fin
145	144	biantru 529	. . . . . 6 ⊢ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin))
146	141, 143, 145	3bitrri 298	. . . . 5 ⊢ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) ↔ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))
147	139, 140	intpr 4938	. . . . . 6 ⊢ ∩ {𝑣, 𝑢} = (𝑣 ∩ 𝑢)
148	147	eleq1i 2828	. . . . 5 ⊢ (∩ {𝑣, 𝑢} ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴)
149	138, 146, 148	3imtr3g 295	. . . 4 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∩ 𝑢) ∈ 𝐴))
150	149	ralrimivv 3178	. . 3 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
151	128, 150	impbii 209	. 2 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
152		ineq1 4166	. . . 4 ⊢ (𝑥 = 𝑣 → (𝑥 ∩ 𝑦) = (𝑣 ∩ 𝑦))
153	152	eleq1d 2822	. . 3 ⊢ (𝑥 = 𝑣 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑦) ∈ 𝐴))
154		ineq2 4167	. . . 4 ⊢ (𝑦 = 𝑢 → (𝑣 ∩ 𝑦) = (𝑣 ∩ 𝑢))
155	154	eleq1d 2822	. . 3 ⊢ (𝑦 = 𝑢 → ((𝑣 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴))
156	153, 155	cbvral2vw 3219	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
157		df-3an 1089	. . . 4 ⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin))
158	157	imbi1i 349	. . 3 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
159	158	albii 1821	. 2 ⊢ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
160	151, 156, 159	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  Vcvv 3441   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4286  {csn 4581  {cpr 4583  ∩ cint 4903   class class class wbr 5099  ^◡ccnv 5624  ran crn 5626   “ cima 5628  suc csuc 6320  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –1-1→wf1 6490  –onto→wfo 6491  –1-1-onto→wf1o 6492  ‘cfv 6493  ωcom 7810   ≈ cen 8884  Fincfn 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-br 5100  df-opab 5162  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-om 7811  df-1o 8399  df-2o 8400  df-en 8888  df-fin 8891

This theorem is referenced by:  dffi2  9330  istop2g  22844  neificl  37956