Theorem fiint 9241

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 5314. (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 8926	. . . . . . 7 ⊢ (𝑧 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑧 ≈ 𝑤)
2		nnfi 9106	. . . . . . . . . 10 ⊢ (𝑤 ∈ ω → 𝑤 ∈ Fin)
3		ensymfib 9122	. . . . . . . . . 10 ⊢ (𝑤 ∈ Fin → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
5		breq1 5103	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ 𝑧 ↔ ∅ ≈ 𝑧))
6	5	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧)))
7	6	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
8	7	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
9		breq1 5103	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑡 → (𝑤 ≈ 𝑧 ↔ 𝑡 ≈ 𝑧))
10	9	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧)))
11	10	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
12	11	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
13		breq1 5103	. . . . . . . . . . . . . . . 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 8971	. . . . . . . . . . . . . . . . . . . 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 8907	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑡 ≈ 𝑧 ↔ ∃𝑓 𝑓:suc 𝑡–1-1-onto→𝑧)
32		ssel 3929	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ⊆ 𝐴 → ((𝑓‘𝑡) ∈ 𝑧 → (𝑓‘𝑡) ∈ 𝐴))
33		f1of 6784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡⟶𝑧)
34		vex 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑡 ∈ V
35	34	sucid 6411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑡 ∈ suc 𝑡
36		ffvelcdm 7037	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 “ 𝑡) ⊆ ran 𝑓
42		dff1o2 6789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 ↔ (𝑓 Fn suc 𝑡 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑧))
43	42	simp3bi 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ran 𝑓 = 𝑧)
44	41, 43	sseqtrid 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓 “ 𝑡) ⊆ 𝑧)
45		sstr2 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓 “ 𝑡) ⊆ 𝑧 → (𝑧 ⊆ 𝐴 → (𝑓 “ 𝑡) ⊆ 𝐴))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑧 ⊆ 𝐴 → (𝑓 “ 𝑡) ⊆ 𝐴))
47	46	anim1d 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
48		f1of1 6783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡–1-1→𝑧)
49		sssucid 6409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑡 ⊆ suc 𝑡
50		vex 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
51		f1imaen3g 8967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 “ 𝑡) ∈ V
56		sseq1 3961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ⊆ 𝐴 ↔ (𝑓 “ 𝑡) ⊆ 𝐴))
57		neeq1 2995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ≠ ∅ ↔ (𝑓 “ 𝑡) ≠ ∅))
58	56, 57	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
59		breq2 5104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑡 ≈ 𝑧 ↔ 𝑡 ≈ (𝑓 “ 𝑡)))
60	58, 59	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) ↔ (((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡))))
61		inteq 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ∩ 𝑧 = ∩ (𝑓 “ 𝑡))
62	61	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (∩ 𝑧 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑡) ∈ 𝐴))
63	60, 62	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴)))
64	55, 63	spcv 3561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
65	54, 64	sylan9 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓:suc 𝑡–1-1-onto→𝑧 ∧ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)) → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
66		ineq1 4167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → (𝑣 ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ 𝑢))
67	66	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → ((𝑣 ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴))
68		ineq2 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 = (𝑓‘𝑡) → (∩ (𝑓 “ 𝑡) ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)))
69	68	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 = (𝑓‘𝑡) → ((∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
70	67, 69	rspc2v 3589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = ∩ ∅)
79		int0 4919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∩ ∅ = V
80	78, 79	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = V)
81	80	ineq1d 4173	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (V ∩ (𝑓‘𝑡)))
82		ssv 3960	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑡) ⊆ V
83		sseqin2 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑡) ∈ V
91	90	intunsn 4944	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡))
92		f1ofn 6785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓 Fn suc 𝑡)
93		fnsnfv 6923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑡 ∧ 𝑡 ∈ suc 𝑡) → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
94	92, 35, 93	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
95	94	uneq2d 4122	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})))
96		df-suc 6333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑡 = (𝑡 ∪ {𝑡})
97	96	imaeq2i 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑡) = (𝑓 “ (𝑡 ∪ {𝑡}))
98		imaundi 6117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑡 ∪ {𝑡})) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡}))
99	97, 98	eqtr2i 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})) = (𝑓 “ suc 𝑡)
100	95, 99	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (𝑓 “ suc 𝑡))
101		f1ofo 6791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡–onto→𝑧)
102		foima 6761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4909	. . . . . . . . . . . . . . . . . . . . . . . . 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 7852	. . . . . . . . . . . 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 3132	. . . . . . 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 5382	. . . . . 6 ⊢ {𝑣, 𝑢} ∈ V
130		sseq1 3961	. . . . . . . . 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 4907	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ∩ 𝑧 = ∩ {𝑣, 𝑢})
136	135	eleq1d 2822	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (∩ 𝑧 ∈ 𝐴 ↔ ∩ {𝑣, 𝑢} ∈ 𝐴))
137	134, 136	imbi12d 344	. . . . . 6 ⊢ (𝑧 = {𝑣, 𝑢} → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴)))
138	129, 137	spcv 3561	. . . . 5 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴))
139		vex 3446	. . . . . . 7 ⊢ 𝑣 ∈ V
140		vex 3446	. . . . . . 7 ⊢ 𝑢 ∈ V
141	139, 140	prss 4778	. . . . . 6 ⊢ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ↔ {𝑣, 𝑢} ⊆ 𝐴)
142	139	prnz 4736	. . . . . . 7 ⊢ {𝑣, 𝑢} ≠ ∅
143	142	biantru 529	. . . . . 6 ⊢ ({𝑣, 𝑢} ⊆ 𝐴 ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅))
144		prfi 9238	. . . . . . 7 ⊢ {𝑣, 𝑢} ∈ Fin
145	144	biantru 529	. . . . . 6 ⊢ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin))
146	141, 143, 145	3bitrri 298	. . . . 5 ⊢ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) ↔ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))
147	139, 140	intpr 4939	. . . . . 6 ⊢ ∩ {𝑣, 𝑢} = (𝑣 ∩ 𝑢)
148	147	eleq1i 2828	. . . . 5 ⊢ (∩ {𝑣, 𝑢} ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴)
149	138, 146, 148	3imtr3g 295	. . . 4 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∩ 𝑢) ∈ 𝐴))
150	149	ralrimivv 3179	. . 3 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
151	128, 150	impbii 209	. 2 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
152		ineq1 4167	. . . 4 ⊢ (𝑥 = 𝑣 → (𝑥 ∩ 𝑦) = (𝑣 ∩ 𝑦))
153	152	eleq1d 2822	. . 3 ⊢ (𝑥 = 𝑣 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑦) ∈ 𝐴))
154		ineq2 4168	. . . 4 ⊢ (𝑦 = 𝑢 → (𝑣 ∩ 𝑦) = (𝑣 ∩ 𝑢))
155	154	eleq1d 2822	. . 3 ⊢ (𝑦 = 𝑢 → ((𝑣 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴))
156	153, 155	cbvral2vw 3220	. 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 3062  Vcvv 3442   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  {csn 4582  {cpr 4584  ∩ cint 4904   class class class wbr 5100  ^◡ccnv 5633  ran crn 5635   “ cima 5637  suc csuc 6329  Fun wfun 6496   Fn wfn 6497  ⟶wf 6498  –1-1→wf1 6499  –onto→wfo 6500  –1-1-onto→wf1o 6501  ‘cfv 6502  ωcom 7820   ≈ cen 8894  Fincfn 8897

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 5245  ax-nul 5255  ax-pr 5381  ax-un 7692

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 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-br 5101  df-opab 5163  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-om 7821  df-1o 8409  df-2o 8410  df-en 8898  df-fin 8901

This theorem is referenced by:  dffi2  9340  istop2g  22857  neificl  38033