Theorem fiint 9363

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 5370. (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 9014	. . . . . . 7 ⊢ (𝑧 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑧 ≈ 𝑤)
2		nnfi 9205	. . . . . . . . . 10 ⊢ (𝑤 ∈ ω → 𝑤 ∈ Fin)
3		ensymfib 9221	. . . . . . . . . 10 ⊢ (𝑤 ∈ Fin → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
5		breq1 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ 𝑧 ↔ ∅ ≈ 𝑧))
6	5	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧)))
7	6	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
8	7	albidv 1917	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
9		breq1 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑡 → (𝑤 ≈ 𝑧 ↔ 𝑡 ≈ 𝑧))
10	9	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧)))
11	10	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
12	11	albidv 1917	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
13		breq1 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = suc 𝑡 → (𝑤 ≈ 𝑧 ↔ suc 𝑡 ≈ 𝑧))
14	13	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = suc 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧)))
15	14	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = suc 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
16	15	albidv 1917	. . . . . . . . . . . . 13 ⊢ (𝑤 = suc 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
17		en0r 9058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ≈ 𝑧 ↔ 𝑧 = ∅)
18	17	biimpi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑧 → 𝑧 = ∅)
19	18	anim1i 615	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ≈ 𝑧 ∧ 𝑧 ≠ ∅) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
20	19	ancoms 458	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ≠ ∅ ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
21	20	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
22		df-ne 2938	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ ↔ ¬ 𝑧 = ∅)
23		pm3.24 402	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (𝑧 = ∅ ∧ ¬ 𝑧 = ∅)
24	23	pm2.21i 119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = ∅ ∧ ¬ 𝑧 = ∅) → ∩ 𝑧 ∈ 𝐴)
25	22, 24	sylan2b 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = ∅ ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ 𝐴)
26	21, 25	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
27	26	ax-gen 1791	. . . . . . . . . . . . . 14 ⊢ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
28	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))
29		nfv 1911	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴
30		nfa1 2148	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
31		bren 8993	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑡 ≈ 𝑧 ↔ ∃𝑓 𝑓:suc 𝑡–1-1-onto→𝑧)
32		ssel 3988	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ⊆ 𝐴 → ((𝑓‘𝑡) ∈ 𝑧 → (𝑓‘𝑡) ∈ 𝐴))
33		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡⟶𝑧)
34		vex 3481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑡 ∈ V
35	34	sucid 6467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑡 ∈ suc 𝑡
36		ffvelcdm 7100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:suc 𝑡⟶𝑧 ∧ 𝑡 ∈ suc 𝑡) → (𝑓‘𝑡) ∈ 𝑧)
37	33, 35, 36	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . 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 2938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 “ 𝑡) ≠ ∅ ↔ ¬ (𝑓 “ 𝑡) = ∅)
41		imassrn 6090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 “ 𝑡) ⊆ ran 𝑓
42		dff1o2 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 ↔ (𝑓 Fn suc 𝑡 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑧))
43	42	simp3bi 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ran 𝑓 = 𝑧)
44	41, 43	sseqtrid 4047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓 “ 𝑡) ⊆ 𝑧)
45		sstr2 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓 “ 𝑡) ⊆ 𝑧 → (𝑧 ⊆ 𝐴 → (𝑓 “ 𝑡) ⊆ 𝐴))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑧 ⊆ 𝐴 → (𝑓 “ 𝑡) ⊆ 𝐴))
47	46	anim1d 611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
48		f1of1 6847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡–1-1→𝑧)
49		sssucid 6465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑡 ⊆ suc 𝑡
50		vex 3481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
51		f1imaen3g 9054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓:suc 𝑡–1-1→𝑧 ∧ 𝑡 ⊆ suc 𝑡 ∧ 𝑓 ∈ V) → 𝑡 ≈ (𝑓 “ 𝑡))
52	49, 50, 51	mp3an23 1452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 “ 𝑡) ∈ V
56		sseq1 4020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ⊆ 𝐴 ↔ (𝑓 “ 𝑡) ⊆ 𝐴))
57		neeq1 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ≠ ∅ ↔ (𝑓 “ 𝑡) ≠ ∅))
58	56, 57	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
59		breq2 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑡 ≈ 𝑧 ↔ 𝑡 ≈ (𝑓 “ 𝑡)))
60	58, 59	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) ↔ (((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡))))
61		inteq 4953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ∩ 𝑧 = ∩ (𝑓 “ 𝑡))
62	61	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (∩ 𝑧 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑡) ∈ 𝐴))
63	60, 62	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴)))
64	55, 63	spcv 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
65	54, 64	sylan9 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓:suc 𝑡–1-1-onto→𝑧 ∧ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)) → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
66		ineq1 4220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → (𝑣 ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ 𝑢))
67	66	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → ((𝑣 ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴))
68		ineq2 4221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 = (𝑓‘𝑡) → (∩ (𝑓 “ 𝑡) ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)))
69	68	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 = (𝑓‘𝑡) → ((∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
70	67, 69	rspc2v 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = ∩ ∅)
79		int0 4966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∩ ∅ = V
80	78, 79	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = V)
81	80	ineq1d 4226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (V ∩ (𝑓‘𝑡)))
82		ssv 4019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑡) ⊆ V
83		sseqin2 4230	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓‘𝑡) ⊆ V ↔ (V ∩ (𝑓‘𝑡)) = (𝑓‘𝑡))
84	82, 83	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (V ∩ (𝑓‘𝑡)) = (𝑓‘𝑡)
85	81, 84	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (𝑓‘𝑡))
86	85	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 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 6919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑡) ∈ V
91	90	intunsn 4991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡))
92		f1ofn 6849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓 Fn suc 𝑡)
93		fnsnfv 6987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑡 ∧ 𝑡 ∈ suc 𝑡) → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
94	92, 35, 93	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
95	94	uneq2d 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})))
96		df-suc 6391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑡 = (𝑡 ∪ {𝑡})
97	96	imaeq2i 6077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑡) = (𝑓 “ (𝑡 ∪ {𝑡}))
98		imaundi 6171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑡 ∪ {𝑡})) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡}))
99	97, 98	eqtr2i 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})) = (𝑓 “ suc 𝑡)
100	95, 99	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (𝑓 “ suc 𝑡))
101		f1ofo 6855	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡–onto→𝑧)
102		foima 6825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–onto→𝑧 → (𝑓 “ suc 𝑡) = 𝑧)
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓 “ suc 𝑡) = 𝑧)
104	100, 103	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = 𝑧)
105	104	inteqd 4955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ∩ 𝑧)
106	91, 105	eqtr3id 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = ∩ 𝑧)
107	106	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴 ↔ ∩ 𝑧 ∈ 𝐴))
108	107	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 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 1930	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ⊆ 𝐴 → (∃𝑓 𝑓:suc 𝑡–1-1-onto→𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
112	31, 111	biimtrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ 𝐴 → (suc 𝑡 ≈ 𝑧 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴))))
113	112	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ⊆ 𝐴 ∧ suc 𝑡 ≈ 𝑧) → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
114	113	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
115	114	com13 88	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
116	29, 30, 115	alrimd 2212	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
117	116	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))))
118	8, 12, 16, 28, 117	finds2 7920	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
119		sp 2180	. . . . . . . . . . . 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 3145	. . . . . . 7 ⊢ (∃𝑤 ∈ ω 𝑧 ≈ 𝑤 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
125	1, 124	sylbi 217	. . . . . 6 ⊢ (𝑧 ∈ Fin → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
126	125	com13 88	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (𝑧 ∈ Fin → ∩ 𝑧 ∈ 𝐴)))
127	126	impd 410	. . . 4 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
128	127	alrimiv 1924	. . 3 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
129		zfpair2 5438	. . . . . 6 ⊢ {𝑣, 𝑢} ∈ V
130		sseq1 4020	. . . . . . . . 9 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ⊆ 𝐴 ↔ {𝑣, 𝑢} ⊆ 𝐴))
131		neeq1 3000	. . . . . . . . 9 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ≠ ∅ ↔ {𝑣, 𝑢} ≠ ∅))
132	130, 131	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅)))
133		eleq1 2826	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ∈ Fin ↔ {𝑣, 𝑢} ∈ Fin))
134	132, 133	anbi12d 632	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin)))
135		inteq 4953	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ∩ 𝑧 = ∩ {𝑣, 𝑢})
136	135	eleq1d 2823	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (∩ 𝑧 ∈ 𝐴 ↔ ∩ {𝑣, 𝑢} ∈ 𝐴))
137	134, 136	imbi12d 344	. . . . . 6 ⊢ (𝑧 = {𝑣, 𝑢} → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴)))
138	129, 137	spcv 3604	. . . . 5 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴))
139		vex 3481	. . . . . . 7 ⊢ 𝑣 ∈ V
140		vex 3481	. . . . . . 7 ⊢ 𝑢 ∈ V
141	139, 140	prss 4824	. . . . . 6 ⊢ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ↔ {𝑣, 𝑢} ⊆ 𝐴)
142	139	prnz 4781	. . . . . . 7 ⊢ {𝑣, 𝑢} ≠ ∅
143	142	biantru 529	. . . . . 6 ⊢ ({𝑣, 𝑢} ⊆ 𝐴 ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅))
144		prfi 9360	. . . . . . 7 ⊢ {𝑣, 𝑢} ∈ Fin
145	144	biantru 529	. . . . . 6 ⊢ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin))
146	141, 143, 145	3bitrri 298	. . . . 5 ⊢ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) ↔ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))
147	139, 140	intpr 4986	. . . . . 6 ⊢ ∩ {𝑣, 𝑢} = (𝑣 ∩ 𝑢)
148	147	eleq1i 2829	. . . . 5 ⊢ (∩ {𝑣, 𝑢} ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴)
149	138, 146, 148	3imtr3g 295	. . . 4 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∩ 𝑢) ∈ 𝐴))
150	149	ralrimivv 3197	. . 3 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
151	128, 150	impbii 209	. 2 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
152		ineq1 4220	. . . 4 ⊢ (𝑥 = 𝑣 → (𝑥 ∩ 𝑦) = (𝑣 ∩ 𝑦))
153	152	eleq1d 2823	. . 3 ⊢ (𝑥 = 𝑣 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑦) ∈ 𝐴))
154		ineq2 4221	. . . 4 ⊢ (𝑦 = 𝑢 → (𝑣 ∩ 𝑦) = (𝑣 ∩ 𝑢))
155	154	eleq1d 2823	. . 3 ⊢ (𝑦 = 𝑢 → ((𝑣 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴))
156	153, 155	cbvral2vw 3238	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
157		df-3an 1088	. . . 4 ⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin))
158	157	imbi1i 349	. . 3 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
159	158	albii 1815	. 2 ⊢ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
160	151, 156, 159	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ∪ cun 3960   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  {csn 4630  {cpr 4632  ∩ cint 4950   class class class wbr 5147  ^◡ccnv 5687  ran crn 5689   “ cima 5691  suc csuc 6387  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  –1-1→wf1 6559  –onto→wfo 6560  –1-1-onto→wf1o 6561  ‘cfv 6562  ωcom 7886   ≈ cen 8980  Fincfn 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-om 7887  df-1o 8504  df-2o 8505  df-en 8984  df-fin 8987

This theorem is referenced by:  dffi2  9460  istop2g  22917  neificl  37739