Theorem fiint 4540

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite non-empty subcollection of A is in A." 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.

Assertion

Ref	Expression
fiint	⊢ (∀x ∈ A ∀y ∈ A (x ∩ y) ∈ A ↔ ∀x((x ⊆ A ⋀ x ≠ ∅ ⋀ ∃y ∈ ω x ≈ y) → ∩x ∈ A))

Distinct variable group:   x,y,A

Proof of Theorem fiint

Step	Hyp	Ref	Expression
1		breq1 2617	. . . . . . . . . . . . . . 15 ⊢ (y = ∅ → (y ≈ x ↔ ∅ ≈ x))
2	1	anbi2d 615	. . . . . . . . . . . . . 14 ⊢ (y = ∅ → (((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) ↔ ((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x)))
3	2	imbi1d 612	. . . . . . . . . . . . 13 ⊢ (y = ∅ → ((((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) ↔ (((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A)))
4	3	albidv 1276	. . . . . . . . . . . 12 ⊢ (y = ∅ → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) ↔ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A)))
5		breq1 2617	. . . . . . . . . . . . . . 15 ⊢ (y = v → (y ≈ x ↔ v ≈ x))
6	5	anbi2d 615	. . . . . . . . . . . . . 14 ⊢ (y = v → (((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) ↔ ((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x)))
7	6	imbi1d 612	. . . . . . . . . . . . 13 ⊢ (y = v → ((((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) ↔ (((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A)))
8	7	albidv 1276	. . . . . . . . . . . 12 ⊢ (y = v → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) ↔ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A)))
9		breq1 2617	. . . . . . . . . . . . . . 15 ⊢ (y = suc v → (y ≈ x ↔ suc v ≈ x))
10	9	anbi2d 615	. . . . . . . . . . . . . 14 ⊢ (y = suc v → (((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) ↔ ((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x)))
11	10	imbi1d 612	. . . . . . . . . . . . 13 ⊢ (y = suc v → ((((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) ↔ (((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x) → ∩x ∈ A)))
12	11	albidv 1276	. . . . . . . . . . . 12 ⊢ (y = suc v → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) ↔ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x) → ∩x ∈ A)))
13		visset 1809	. . . . . . . . . . . . . . . . . . . 20 ⊢ x ∈ V
14	13	ensym 4399	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ x → x ≈ ∅)
15		en0 4410	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ≈ ∅ ↔ x = ∅)
16	14, 15	sylib 198	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ≈ x → x = ∅)
17	16	anim1i 334	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ≈ x ⋀ x ≠ ∅) → (x = ∅ ⋀ x ≠ ∅))
18	17	ancoms 436	. . . . . . . . . . . . . . . 16 ⊢ ((x ≠ ∅ ⋀ ∅ ≈ x) → (x = ∅ ⋀ x ≠ ∅))
19	18	adantll 392	. . . . . . . . . . . . . . 15 ⊢ (((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → (x = ∅ ⋀ x ≠ ∅))
20		pm3.24 657	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (x = ∅ ⋀ ¬ x = ∅)
21	20	pm2.21i 77	. . . . . . . . . . . . . . . 16 ⊢ ((x = ∅ ⋀ ¬ x = ∅) → ∩x ∈ A)
22		df-ne 1584	. . . . . . . . . . . . . . . 16 ⊢ (x ≠ ∅ ↔ ¬ x = ∅)
23	21, 22	sylan2b 452	. . . . . . . . . . . . . . 15 ⊢ ((x = ∅ ⋀ x ≠ ∅) → ∩x ∈ A)
24	19, 23	syl 10	. . . . . . . . . . . . . 14 ⊢ (((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A)
25	24	ax-gen 961	. . . . . . . . . . . . 13 ⊢ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A)
26	25	a1i 8	. . . . . . . . . . . 12 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A))
27		ax-17 969	. . . . . . . . . . . . . 14 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)
28		hba1 1001	. . . . . . . . . . . . . 14 ⊢ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → ∀x∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A))
29		ssel 2059	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ⊆ A → ((f ‘v) ∈ x → (f ‘v) ∈ A))
30		f1ofo 3686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–1-1-onto→x → f:suc v–onto→x)
31		fof 3663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–onto→x → f:suc v–→x)
32		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ v ∈ V
33	32	sucid 3046	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ v ∈ suc v
34		ffvelrn 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f:suc v–→x ⋀ v ∈ suc v) → (f ‘v) ∈ x)
35	33, 34	mpan2 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–→x → (f ‘v) ∈ x)
36	30, 31, 35	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc v–1-1-onto→x → (f ‘v) ∈ x)
37	29, 36	syl5 21	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x ⊆ A → (f:suc v–1-1-onto→x → (f ‘v) ∈ A))
38	37	imp 350	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((x ⊆ A ⋀ f:suc v–1-1-onto→x) → (f ‘v) ∈ A)
39	38	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → (f ‘v) ∈ A)
40		imassrn 3407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (f “ v) ⊆ ran f
41		f1o2 3684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (f:suc v–1-1-onto→x ↔ (f Fn suc v ⋀ Fun ◡f ⋀ ran f = x))
42		3simp3 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((f Fn suc v ⋀ Fun ◡f ⋀ ran f = x) → ran f = x)
43	41, 42	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (f:suc v–1-1-onto→x → ran f = x)
44	43	sseq2d 2085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ⊆ ran f ↔ (f “ v) ⊆ x))
45	40, 44	mpbii 193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (f:suc v–1-1-onto→x → (f “ v) ⊆ x)
46		sstr2 2067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((f “ v) ⊆ x → (x ⊆ A → (f “ v) ⊆ A))
47	45, 46	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f:suc v–1-1-onto→x → (x ⊆ A → (f “ v) ⊆ A))
48	47	anim1d 559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc v–1-1-onto→x → ((x ⊆ A ⋀ (f “ v) ≠ ∅) → ((f “ v) ⊆ A ⋀ (f “ v) ≠ ∅)))
49		f1of1 3679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f:suc v–1-1-onto→x → f:suc v–1-1→x)
50		sssucid 3042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ v ⊆ suc v
51		f1ores 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((f:suc v–1-1→x ⋀ v ⊆ suc v) → (f ↾ v):v–1-1-onto→(f “ v))
52	50, 51	mpan2 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f:suc v–1-1→x → (f ↾ v):v–1-1-onto→(f “ v))
53	32	f1oen 4385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((f ↾ v):v–1-1-onto→(f “ v) → v ≈ (f “ v))
54	49, 52, 53	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc v–1-1-onto→x → v ≈ (f “ v))
55	48, 54	jctird 601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f:suc v–1-1-onto→x → ((x ⊆ A ⋀ (f “ v) ≠ ∅) → (((f “ v) ⊆ A ⋀ (f “ v) ≠ ∅) ⋀ v ≈ (f “ v))))
56		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ f ∈ V
57		imaexg 3408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f ∈ V → (f “ v) ∈ V)
58	56, 57	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f “ v) ∈ V
59		sseq1 2078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (x = (f “ v) → (x ⊆ A ↔ (f “ v) ⊆ A))
60		neeq1 1587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (x = (f “ v) → (x ≠ ∅ ↔ (f “ v) ≠ ∅))
61	59, 60	anbi12d 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (x = (f “ v) → ((x ⊆ A ⋀ x ≠ ∅) ↔ ((f “ v) ⊆ A ⋀ (f “ v) ≠ ∅)))
62		breq2 2618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (x = (f “ v) → (v ≈ x ↔ v ≈ (f “ v)))
63	61, 62	anbi12d 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (x = (f “ v) → (((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) ↔ (((f “ v) ⊆ A ⋀ (f “ v) ≠ ∅) ⋀ v ≈ (f “ v))))
64		inteq 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (x = (f “ v) → ∩x = ∩(f “ v))
65	64	eleq1d 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (x = (f “ v) → (∩x ∈ A ↔ ∩(f “ v) ∈ A))
66	63, 65	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (x = (f “ v) → ((((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ↔ ((((f “ v) ⊆ A ⋀ (f “ v) ≠ ∅) ⋀ v ≈ (f “ v)) → ∩(f “ v) ∈ A)))
67	58, 66	cla4v 1864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → ((((f “ v) ⊆ A ⋀ (f “ v) ≠ ∅) ⋀ v ≈ (f “ v)) → ∩(f “ v) ∈ A))
68	55, 67	sylan9 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((f:suc v–1-1-onto→x ⋀ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A)) → ((x ⊆ A ⋀ (f “ v) ≠ ∅) → ∩(f “ v) ∈ A))
69		ineq1 2206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (z = ∩(f “ v) → (z ∩ w) = (∩(f “ v) ∩ w))
70	69	eleq1d 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (z = ∩(f “ v) → ((z ∩ w) ∈ A ↔ (∩(f “ v) ∩ w) ∈ A))
71		ineq2 2207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (w = (f ‘v) → (∩(f “ v) ∩ w) = (∩(f “ v) ∩ (f ‘v)))
72	71	eleq1d 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (w = (f ‘v) → ((∩(f “ v) ∩ w) ∈ A ↔ (∩(f “ v) ∩ (f ‘v)) ∈ A))
73	70, 72	rcla42v 1876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∩(f “ v) ∈ A ⋀ (f ‘v) ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))
74	73	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∩(f “ v) ∈ A → ((f ‘v) ∈ A → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A)))
75	68, 74	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((f:suc v–1-1-onto→x ⋀ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A)) → ((x ⊆ A ⋀ (f “ v) ≠ ∅) → ((f ‘v) ∈ A → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))))
76	75	com4r 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((f:suc v–1-1-onto→x ⋀ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A)) → ((x ⊆ A ⋀ (f “ v) ≠ ∅) → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))))
77	76	exp4a 378	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((f:suc v–1-1-onto→x ⋀ ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A)) → (x ⊆ A → ((f “ v) ≠ ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A)))))
78	77	exp3a 375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (f:suc v–1-1-onto→x → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (x ⊆ A → ((f “ v) ≠ ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))))))
79	78	com14 38	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ⊆ A → (f:suc v–1-1-onto→x → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((f “ v) ≠ ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))))))
80	79	imp43 370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → ((f “ v) ≠ ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A)))
81		df-ne 1584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f “ v) ≠ ∅ ↔ ¬ (f “ v) = ∅)
82	80, 81	syl5ibr 207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → (¬ (f “ v) = ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A)))
83		inteq 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f “ v) = ∅ → ∩(f “ v) = ∩∅)
84		int0 2542	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∩∅ = V
85	83, 84	syl6eq 1520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f “ v) = ∅ → ∩(f “ v) = V)
86	85	ineq1d 2212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f “ v) = ∅ → (∩(f “ v) ∩ (f ‘v)) = (V ∩ (f ‘v)))
87		ssv 2077	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f ‘v) ⊆ V
88		sseqin2 2225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f ‘v) ⊆ V ↔ (V ∩ (f ‘v)) = (f ‘v))
89	87, 88	mpbi 189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (V ∩ (f ‘v)) = (f ‘v)
90	86, 89	syl6eq 1520	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f “ v) = ∅ → (∩(f “ v) ∩ (f ‘v)) = (f ‘v))
91	90	eleq1d 1537	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f “ v) = ∅ → ((∩(f “ v) ∩ (f ‘v)) ∈ A ↔ (f ‘v) ∈ A))
92	91	biimprd 154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f “ v) = ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))
93	82, 92	pm2.61d2 129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))
94	39, 93	mpd 26	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → (∩(f “ v) ∩ (f ‘v)) ∈ A)
95		f1ofn 3681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc v–1-1-onto→x → f Fn suc v)
96		fnsnfv 3758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((f Fn suc v ⋀ v ∈ suc v) → {(f ‘v)} = (f “ {v}))
97	33, 96	mpan2 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f Fn suc v → {(f ‘v)} = (f “ {v}))
98	95, 97	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f:suc v–1-1-onto→x → {(f ‘v)} = (f “ {v}))
99	98	uneq2d 2180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ∪ {(f ‘v)}) = ((f “ v) ∪ (f “ {v})))
100		df-suc 2949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ suc v = (v ∪ {v})
101		imaeq2 3394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (suc v = (v ∪ {v}) → (f “ suc v) = (f “ (v ∪ {v})))
102	100, 101	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f “ suc v) = (f “ (v ∪ {v}))
103		imaun 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f “ (v ∪ {v})) = ((f “ v) ∪ (f “ {v}))
104	102, 103	eqtr2 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f “ v) ∪ (f “ {v})) = (f “ suc v)
105	99, 104	syl6eq 1520	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ∪ {(f ‘v)}) = (f “ suc v))
106		foima 3667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc v–onto→x → (f “ suc v) = x)
107	30, 106	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–1-1-onto→x → (f “ suc v) = x)
108	105, 107	eqtrd 1504	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ∪ {(f ‘v)}) = x)
109	108	inteqd 2533	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc v–1-1-onto→x → ∩((f “ v) ∪ {(f ‘v)}) = ∩x)
110		fvex 3723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f ‘v) ∈ V
111	110	intunsn 2560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∩((f “ v) ∪ {(f ‘v)}) = (∩(f “ v) ∩ (f ‘v))
112	109, 111	syl5eqr 1518	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f:suc v–1-1-onto→x → (∩(f “ v) ∩ (f ‘v)) = ∩x)
113	112	eleq1d 1537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc v–1-1-onto→x → ((∩(f “ v) ∩ (f ‘v)) ∈ A ↔ ∩x ∈ A))
114	113	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → ((∩(f “ v) ∩ (f ‘v)) ∈ A ↔ ∩x ∈ A))
115	94, 114	mpbid 195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((x ⊆ A ⋀ f:suc v–1-1-onto→x) ⋀ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) ⋀ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)) → ∩x ∈ A)
116	115	exp43 384	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ⊆ A → (f:suc v–1-1-onto→x → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
117	116	19.23adv 1212	. . . . . . . . . . . . . . . . . 18 ⊢ (x ⊆ A → (∃f f:suc v–1-1-onto→x → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
118	13	bren 4365	. . . . . . . . . . . . . . . . . 18 ⊢ (suc v ≈ x ↔ ∃f f:suc v–1-1-onto→x)
119	117, 118	syl5ib 206	. . . . . . . . . . . . . . . . 17 ⊢ (x ⊆ A → (suc v ≈ x → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
120	119	imp 350	. . . . . . . . . . . . . . . 16 ⊢ ((x ⊆ A ⋀ suc v ≈ x) → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A)))
121	120	adantlr 393	. . . . . . . . . . . . . . 15 ⊢ (((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x) → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A)))
122	121	com13 33	. . . . . . . . . . . . . 14 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → (((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x) → ∩x ∈ A)))
123	27, 28, 122	19.21ad 1057	. . . . . . . . . . . . 13 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x) → ∩x ∈ A)))
124	123	a1i 8	. . . . . . . . . . . 12 ⊢ (v ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x) → ∩x ∈ A) → ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x) → ∩x ∈ A))))
125	4, 8, 12, 26, 124	finds2 3153	. . . . . . . . . . 11 ⊢ (y ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A)))
126		ax-4 971	. . . . . . . . . . 11 ⊢ (∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A) → (((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A))
127	125, 126	syl6 22	. . . . . . . . . 10 ⊢ (y ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (((x ⊆ A ⋀ x ≠ ∅) ⋀ y ≈ x) → ∩x ∈ A)))
128	127	exp4a 378	. . . . . . . . 9 ⊢ (y ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((x ⊆ A ⋀ x ≠ ∅) → (y ≈ x → ∩x ∈ A))))
129	128	com24 37	. . . . . . . 8 ⊢ (y ∈ ω → (y ≈ x → ((x ⊆ A ⋀ x ≠ ∅) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
130		visset 1809	. . . . . . . . 9 ⊢ y ∈ V
131	130	ensym 4399	. . . . . . . 8 ⊢ (x ≈ y → y ≈ x)
132	129, 131	syl5 21	. . . . . . 7 ⊢ (y ∈ ω → (x ≈ y → ((x ⊆ A ⋀ x ≠ ∅) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
133	132	r19.23aiv 1740	. . . . . 6 ⊢ (∃y ∈ ω x ≈ y → ((x ⊆ A ⋀ x ≠ ∅) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A)))
134	133	com13 33	. . . . 5 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((x ⊆ A ⋀ x ≠ ∅) → (∃y ∈ ω x ≈ y → ∩x ∈ A)))
135	134	imp3a 361	. . . 4 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (((x ⊆ A ⋀ x ≠ ∅) ⋀ ∃y ∈ ω x ≈ y) → ∩x ∈ A))
136	135	19.21aiv 1284	. . 3 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x(((x ⊆ A ⋀ x ≠ ∅) ⋀ ∃y ∈ ω x ≈ y) → ∩x ∈ A))
137		zfpair2 2775	. . . . . 6 ⊢ {z, w} ∈ V
138		sseq1 2078	. . . . . . . . 9 ⊢ (x = {z, w} → (x ⊆ A ↔ {z, w} ⊆ A))
139		neeq1 1587	. . . . . . . . 9 ⊢ (x = {z, w} → (x ≠ ∅ ↔ {z, w} ≠ ∅))
140	138, 139	anbi12d 627	. . . . . . . 8 ⊢ (x = {z, w} → ((x ⊆ A ⋀ x ≠ ∅) ↔ ({z, w} ⊆ A ⋀ {z, w} ≠ ∅)))
141		breq1 2617	. . . . . . . . 9 ⊢ (x = {z, w} → (x ≈ y ↔ {z, w} ≈ y))
142	141	rexbidv 1661	. . . . . . . 8 ⊢ (x = {z, w} → (∃y ∈ ω x ≈ y ↔ ∃y ∈ ω {z, w} ≈ y))
143	140, 142	anbi12d 627	. . . . . . 7 ⊢ (x = {z, w} → (((x ⊆ A ⋀ x ≠ ∅) ⋀ ∃y ∈ ω x ≈ y) ↔ (({z, w} ⊆ A ⋀ {z, w} ≠ ∅) ⋀ ∃y ∈ ω {z, w} ≈ y)))
144		inteq 2531	. . . . . . . 8 ⊢ (x = {z, w} → ∩x = ∩{z, w})
145	144	eleq1d 1537	. . . . . . 7 ⊢ (x = {z, w} → (∩x ∈ A ↔ ∩{z, w} ∈ A))
146	143, 145	imbi12d 625	. . . . . 6 ⊢ (x = {z, w} → ((((x ⊆ A ⋀ x ≠ ∅) ⋀ ∃y ∈ ω x ≈ y) → ∩x ∈ A) ↔ ((({z, w} ⊆ A ͹