Theorem fiint 9366

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 5365. (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 9016	. . . . . . 7 ⊢ (𝑧 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑧 ≈ 𝑤)
2		nnfi 9207	. . . . . . . . . 10 ⊢ (𝑤 ∈ ω → 𝑤 ∈ Fin)
3		ensymfib 9224	. . . . . . . . . 10 ⊢ (𝑤 ∈ Fin → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → (𝑤 ≈ 𝑧 ↔ 𝑧 ≈ 𝑤))
5		breq1 5146	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ 𝑧 ↔ ∅ ≈ 𝑧))
6	5	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧)))
7	6	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
8	7	albidv 1920	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
9		breq1 5146	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑡 → (𝑤 ≈ 𝑧 ↔ 𝑡 ≈ 𝑧))
10	9	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧)))
11	10	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
12	11	albidv 1920	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
13		breq1 5146	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = suc 𝑡 → (𝑤 ≈ 𝑧 ↔ suc 𝑡 ≈ 𝑧))
14	13	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = suc 𝑡 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧)))
15	14	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑤 = suc 𝑡 → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
16	15	albidv 1920	. . . . . . . . . . . . 13 ⊢ (𝑤 = suc 𝑡 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
17		en0r 9060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ≈ 𝑧 ↔ 𝑧 = ∅)
18	17	biimpi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑧 → 𝑧 = ∅)
19	18	anim1i 615	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ≈ 𝑧 ∧ 𝑧 ≠ ∅) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
20	19	ancoms 458	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ≠ ∅ ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
21	20	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
22		df-ne 2941	. . . . . . . . . . . . . . . . 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 1795	. . . . . . . . . . . . . 14 ⊢ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
28	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))
29		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴
30		nfa1 2151	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)
31		bren 8995	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑡 ≈ 𝑧 ↔ ∃𝑓 𝑓:suc 𝑡–1-1-onto→𝑧)
32		ssel 3977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ⊆ 𝐴 → ((𝑓‘𝑡) ∈ 𝑧 → (𝑓‘𝑡) ∈ 𝐴))
33		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓:suc 𝑡⟶𝑧)
34		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑡 ∈ V
35	34	sucid 6466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑡 ∈ suc 𝑡
36		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2941	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 “ 𝑡) ≠ ∅ ↔ ¬ (𝑓 “ 𝑡) = ∅)
41		imassrn 6089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 “ 𝑡) ⊆ ran 𝑓
42		dff1o2 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 ↔ (𝑓 Fn suc 𝑡 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑧))
43	42	simp3bi 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ran 𝑓 = 𝑧)
44	41, 43	sseqtrid 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (𝑓 “ 𝑡) ⊆ 𝑧)
45		sstr2 3990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑡 ⊆ suc 𝑡
50		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
51		f1imaen3g 9056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓:suc 𝑡–1-1→𝑧 ∧ 𝑡 ⊆ suc 𝑡 ∧ 𝑓 ∈ V) → 𝑡 ≈ (𝑓 “ 𝑡))
52	49, 50, 51	mp3an23 1455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ⊆ 𝐴 ↔ (𝑓 “ 𝑡) ⊆ 𝐴))
57		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑧 ≠ ∅ ↔ (𝑓 “ 𝑡) ≠ ∅))
58	56, 57	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅)))
59		breq2 5147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → (𝑡 ≈ 𝑧 ↔ 𝑡 ≈ (𝑓 “ 𝑡)))
60	58, 59	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) ↔ (((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡))))
61		inteq 4949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑡) → ∩ 𝑧 = ∩ (𝑓 “ 𝑡))
62	61	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑡) → (∩ 𝑧 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑡) ∈ 𝐴))
63	60, 62	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑓 “ 𝑡) → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) ↔ ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴)))
64	55, 63	spcv 3605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ((((𝑓 “ 𝑡) ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓 “ 𝑡)) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
65	54, 64	sylan9 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓:suc 𝑡–1-1-onto→𝑧 ∧ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)) → ((𝑧 ⊆ 𝐴 ∧ (𝑓 “ 𝑡) ≠ ∅) → ∩ (𝑓 “ 𝑡) ∈ 𝐴))
66		ineq1 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → (𝑣 ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ 𝑢))
67	66	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = ∩ (𝑓 “ 𝑡) → ((𝑣 ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴))
68		ineq2 4214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 = (𝑓‘𝑡) → (∩ (𝑓 “ 𝑡) ∩ 𝑢) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)))
69	68	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 = (𝑓‘𝑡) → ((∩ (𝑓 “ 𝑡) ∩ 𝑢) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) ∈ 𝐴))
70	67, 69	rspc2v 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = ∩ ∅)
79		int0 4962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∩ ∅ = V
80	78, 79	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) = ∅ → ∩ (𝑓 “ 𝑡) = V)
81	80	ineq1d 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (V ∩ (𝑓‘𝑡)))
82		ssv 4008	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑡) ⊆ V
83		sseqin2 4223	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓‘𝑡) ⊆ V ↔ (V ∩ (𝑓‘𝑡)) = (𝑓‘𝑡))
84	82, 83	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (V ∩ (𝑓‘𝑡)) = (𝑓‘𝑡)
85	81, 84	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑡) = ∅ → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = (𝑓‘𝑡))
86	85	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . 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 4987	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡))
92		f1ofn 6849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → 𝑓 Fn suc 𝑡)
93		fnsnfv 6988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑡 ∧ 𝑡 ∈ suc 𝑡) → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
94	92, 35, 93	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → {(𝑓‘𝑡)} = (𝑓 “ {𝑡}))
95	94	uneq2d 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})))
96		df-suc 6390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑡 = (𝑡 ∪ {𝑡})
97	96	imaeq2i 6076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑡) = (𝑓 “ (𝑡 ∪ {𝑡}))
98		imaundi 6169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑡 ∪ {𝑡})) = ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡}))
99	97, 98	eqtr2i 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑡) ∪ (𝑓 “ {𝑡})) = (𝑓 “ suc 𝑡)
100	95, 99	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = 𝑧)
105	104	inteqd 4951	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → ∩ ((𝑓 “ 𝑡) ∪ {(𝑓‘𝑡)}) = ∩ 𝑧)
106	91, 105	eqtr3id 2791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑡–1-1-onto→𝑧 → (∩ (𝑓 “ 𝑡) ∩ (𝑓‘𝑡)) = ∩ 𝑧)
107	106	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . 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 1933	. . . . . . . . . . . . . . . . . . 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 2215	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
117	116	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴) → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ suc 𝑡 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴))))
118	8, 12, 16, 28, 117	finds2 7920	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ω → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑤 ≈ 𝑧) → ∩ 𝑧 ∈ 𝐴)))
119		sp 2183	. . . . . . . . . . . 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 3148	. . . . . . 7 ⊢ (∃𝑤 ∈ ω 𝑧 ≈ 𝑤 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
125	1, 124	sylbi 217	. . . . . 6 ⊢ (𝑧 ∈ Fin → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∩ 𝑧 ∈ 𝐴)))
126	125	com13 88	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (𝑧 ∈ Fin → ∩ 𝑧 ∈ 𝐴)))
127	126	impd 410	. . . 4 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
128	127	alrimiv 1927	. . 3 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 → ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
129		zfpair2 5433	. . . . . 6 ⊢ {𝑣, 𝑢} ∈ V
130		sseq1 4009	. . . . . . . . 9 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ⊆ 𝐴 ↔ {𝑣, 𝑢} ⊆ 𝐴))
131		neeq1 3003	. . . . . . . . 9 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ≠ ∅ ↔ {𝑣, 𝑢} ≠ ∅))
132	130, 131	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅)))
133		eleq1 2829	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → (𝑧 ∈ Fin ↔ {𝑣, 𝑢} ∈ Fin))
134	132, 133	anbi12d 632	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin)))
135		inteq 4949	. . . . . . . 8 ⊢ (𝑧 = {𝑣, 𝑢} → ∩ 𝑧 = ∩ {𝑣, 𝑢})
136	135	eleq1d 2826	. . . . . . 7 ⊢ (𝑧 = {𝑣, 𝑢} → (∩ 𝑧 ∈ 𝐴 ↔ ∩ {𝑣, 𝑢} ∈ 𝐴))
137	134, 136	imbi12d 344	. . . . . 6 ⊢ (𝑧 = {𝑣, 𝑢} → ((((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴)))
138	129, 137	spcv 3605	. . . . 5 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → ∩ {𝑣, 𝑢} ∈ 𝐴))
139		vex 3484	. . . . . . 7 ⊢ 𝑣 ∈ V
140		vex 3484	. . . . . . 7 ⊢ 𝑢 ∈ V
141	139, 140	prss 4820	. . . . . 6 ⊢ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ↔ {𝑣, 𝑢} ⊆ 𝐴)
142	139	prnz 4777	. . . . . . 7 ⊢ {𝑣, 𝑢} ≠ ∅
143	142	biantru 529	. . . . . 6 ⊢ ({𝑣, 𝑢} ⊆ 𝐴 ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅))
144		prfi 9363	. . . . . . 7 ⊢ {𝑣, 𝑢} ∈ Fin
145	144	biantru 529	. . . . . 6 ⊢ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin))
146	141, 143, 145	3bitrri 298	. . . . 5 ⊢ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) ↔ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))
147	139, 140	intpr 4982	. . . . . 6 ⊢ ∩ {𝑣, 𝑢} = (𝑣 ∩ 𝑢)
148	147	eleq1i 2832	. . . . 5 ⊢ (∩ {𝑣, 𝑢} ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴)
149	138, 146, 148	3imtr3g 295	. . . 4 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∩ 𝑢) ∈ 𝐴))
150	149	ralrimivv 3200	. . 3 ⊢ (∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) → ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
151	128, 150	impbii 209	. 2 ⊢ (∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴 ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
152		ineq1 4213	. . . 4 ⊢ (𝑥 = 𝑣 → (𝑥 ∩ 𝑦) = (𝑣 ∩ 𝑦))
153	152	eleq1d 2826	. . 3 ⊢ (𝑥 = 𝑣 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑦) ∈ 𝐴))
154		ineq2 4214	. . . 4 ⊢ (𝑦 = 𝑢 → (𝑣 ∩ 𝑦) = (𝑣 ∩ 𝑢))
155	154	eleq1d 2826	. . 3 ⊢ (𝑦 = 𝑢 → ((𝑣 ∩ 𝑦) ∈ 𝐴 ↔ (𝑣 ∩ 𝑢) ∈ 𝐴))
156	153, 155	cbvral2vw 3241	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑣 ∈ 𝐴 ∀𝑢 ∈ 𝐴 (𝑣 ∩ 𝑢) ∈ 𝐴)
157		df-3an 1089	. . . 4 ⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin))
158	157	imbi1i 349	. . 3 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
159	158	albii 1819	. 2 ⊢ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴) ↔ ∀𝑧(((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
160	151, 156, 159	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {csn 4626  {cpr 4628  ∩ cint 4946   class class class wbr 5143  ^◡ccnv 5684  ran crn 5686   “ cima 5688  suc csuc 6386  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557  –1-1→wf1 6558  –onto→wfo 6559  –1-1-onto→wf1o 6560  ‘cfv 6561  ωcom 7887   ≈ cen 8982  Fincfn 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-2o 8507  df-en 8986  df-fin 8989

This theorem is referenced by:  dffi2  9463  istop2g  22902  neificl  37760