Theorem fiint 3445

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(s):   x,y,A

Proof of Theorem fiint

Step	Hyp	Ref	Expression
1		ineq1 1638	. . . . 5 ⊢ (x = z → (x ∩ y) = (z ∩ y))
2	1	eleq1d 1155	. . . 4 ⊢ (x = z → ((x ∩ y) ∈ A ↔ (z ∩ y) ∈ A))
3	2	biraldv 1219	. . 3 ⊢ (x = z → (∀y ∈ A (x ∩ y) ∈ A ↔ ∀y ∈ A (z ∩ y) ∈ A))
4	3	cbvralv 1333	. 2 ⊢ (∀x ∈ A ∀y ∈ A (x ∩ y) ∈ A ↔ ∀z ∈ A ∀y ∈ A (z ∩ y) ∈ A)
5		ineq2 1639	. . . . 5 ⊢ (y = w → (z ∩ y) = (z ∩ w))
6	5	eleq1d 1155	. . . 4 ⊢ (y = w → ((z ∩ y) ∈ A ↔ (z ∩ w) ∈ A))
7	6	cbvralv 1333	. . 3 ⊢ (∀y ∈ A (z ∩ y) ∈ A ↔ ∀w ∈ A (z ∩ w) ∈ A)
8	7	biral 1223	. 2 ⊢ (∀z ∈ A ∀y ∈ A (z ∩ y) ∈ A ↔ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)
9		breq1 2065	. . . . . . . . . . . . . . 15 ⊢ (y = ∅ → (y ≈ x ↔ ∅ ≈ x))
10	9	anbi2d 468	. . . . . . . . . . . . . 14 ⊢ (y = ∅ → (((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) ↔ ((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x)))
11	10	imbi1d 465	. . . . . . . . . . . . 13 ⊢ (y = ∅ → ((((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) ↔ (((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x) → ∩x ∈ A)))
12	11	bialdv 935	. . . . . . . . . . . 12 ⊢ (y = ∅ → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) ↔ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x) → ∩x ∈ A)))
13		breq1 2065	. . . . . . . . . . . . . . 15 ⊢ (y = v → (y ≈ x ↔ v ≈ x))
14	13	anbi2d 468	. . . . . . . . . . . . . 14 ⊢ (y = v → (((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) ↔ ((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x)))
15	14	imbi1d 465	. . . . . . . . . . . . 13 ⊢ (y = v → ((((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) ↔ (((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A)))
16	15	bialdv 935	. . . . . . . . . . . 12 ⊢ (y = v → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) ↔ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A)))
17		breq1 2065	. . . . . . . . . . . . . . 15 ⊢ (y = suc v → (y ≈ x ↔ suc v ≈ x))
18	17	anbi2d 468	. . . . . . . . . . . . . 14 ⊢ (y = suc v → (((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) ↔ ((x ⊆ A ∧ ¬ x = ∅) ∧ suc v ≈ x)))
19	18	imbi1d 465	. . . . . . . . . . . . 13 ⊢ (y = suc v → ((((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) ↔ (((x ⊆ A ∧ ¬ x = ∅) ∧ suc v ≈ x) → ∩x ∈ A)))
20	19	bialdv 935	. . . . . . . . . . . 12 ⊢ (y = suc v → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) ↔ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ suc v ≈ x) → ∩x ∈ A)))
21		visset 1350	. . . . . . . . . . . . . . . . . . . 20 ⊢ x ∈ V
22	21	ensym 3317	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ x → x ≈ ∅)
23		en0 3328	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ≈ ∅ ↔ x = ∅)
24	22, 23	sylib 173	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ≈ x → x = ∅)
25	24	anim1i 269	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ≈ x ∧ ¬ x = ∅) → (x = ∅ ∧ ¬ x = ∅))
26	25	ancoms 334	. . . . . . . . . . . . . . . 16 ⊢ ((¬ x = ∅ ∧ ∅ ≈ x) → (x = ∅ ∧ ¬ x = ∅))
27	26	adantll 309	. . . . . . . . . . . . . . 15 ⊢ (((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x) → (x = ∅ ∧ ¬ x = ∅))
28		pm3.24 496	. . . . . . . . . . . . . . . 16 ⊢ ¬ (x = ∅ ∧ ¬ x = ∅)
29	28	pm2.21i 73	. . . . . . . . . . . . . . 15 ⊢ ((x = ∅ ∧ ¬ x = ∅) → ∩x ∈ A)
30	27, 29	syl 12	. . . . . . . . . . . . . 14 ⊢ (((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x) → ∩x ∈ A)
31	30	ax-gen 677	. . . . . . . . . . . . 13 ⊢ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x) → ∩x ∈ A)
32	31	a1i 7	. . . . . . . . . . . 12 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ ∅ ≈ x) → ∩x ∈ A))
33		ax-17 925	. . . . . . . . . . . . . 14 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A)
34		hba1 698	. . . . . . . . . . . . . 14 ⊢ (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) → ∀x∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A))
35		ssel 1502	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ⊆ A → ((f ‘v) ∈ x → (f ‘v) ∈ A))
36		df-f1o 2437	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc v–1-1-onto→x ↔ (f:suc v–1-1→x ∧ f:suc v–onto→x))
37	36	pm3.27bd 263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–1-1-onto→x → f:suc v–onto→x)
38		fof 2788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–onto→x → f:suc v–→x)
39		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ v ∈ V
40	39	sucid 2304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ v ∈ suc v
41		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f:suc v–→x ∧ v ∈ suc v) → (f ‘v) ∈ x)
42	40, 41	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–→x → (f ‘v) ∈ x)
43	37, 38, 42	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc v–1-1-onto→x → (f ‘v) ∈ x)
44	35, 43	syl5 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x ⊆ A → (f:suc v–1-1-onto→x → (f ‘v) ∈ A))
45	44	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((x ⊆ A ∧ f:suc v–1-1-onto→x) → (f ‘v) ∈ A)
46	45	adantr 306	. . . . . . . . . . . . . . . . . . . . . 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)
47		imassrn 2611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f “ v) ⊆ ran f
48		f1o2 2804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (f:suc v–1-1-onto→x ↔ (f Fn suc v ∧ Fun ◡f ∧ ran f = x))
49		3simp3 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((f Fn suc v ∧ Fun ◡f ∧ ran f = x) → ran f = x)
50	48, 49	sylbi 174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (f:suc v–1-1-onto→x → ran f = x)
51	50	sseq2d 1528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ⊆ ran f ↔ (f “ v) ⊆ x))
52	47, 51	mpbii 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc v–1-1-onto→x → (f “ v) ⊆ x)
53		sstr2 1510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((f “ v) ⊆ x → (x ⊆ A → (f “ v) ⊆ A))
54	52, 53	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f:suc v–1-1-onto→x → (x ⊆ A → (f “ v) ⊆ A))
55	54	anim1d 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f:suc v–1-1-onto→x → ((x ⊆ A ∧ ¬ (f “ v) = ∅) → ((f “ v) ⊆ A ∧ ¬ (f “ v) = ∅)))
56		f1of1 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc v–1-1-onto→x → f:suc v–1-1→x)
57		sssucid 2300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ v ⊆ suc v
58		f1ores 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((f:suc v–1-1→x ∧ v ⊆ suc v) → (f ↾ v):v–1-1-onto→(f “ v))
59	57, 58	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc v–1-1→x → (f ↾ v):v–1-1-onto→(f “ v))
60	39	f1oen 3301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((f ↾ v):v–1-1-onto→(f “ v) → v ≈ (f “ v))
61	56, 59, 60	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f:suc v–1-1-onto→x → v ≈ (f “ v))
62	61	a1d 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f:suc v–1-1-onto→x → ((x ⊆ A ∧ ¬ (f “ v) = ∅) → v ≈ (f “ v)))
63	55, 62	jcad 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc v–1-1-onto→x → ((x ⊆ A ∧ ¬ (f “ v) = ∅) → (((f “ v) ⊆ A ∧ ¬ (f “ v) = ∅) ∧ v ≈ (f “ v))))
64		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ f ∈ V
65		imaexg 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f ∈ V → (f “ v) ∈ V)
66	64, 65	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f “ v) ∈ V
67		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (x = (f “ v) → (x ⊆ A ↔ (f “ v) ⊆ A))
68		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (x = (f “ v) → (x = ∅ ↔ (f “ v) = ∅))
69	68	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (x = (f “ v) → (¬ x = ∅ ↔ ¬ (f “ v) = ∅))
70	67, 69	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (x = (f “ v) → ((x ⊆ A ∧ ¬ x = ∅) ↔ ((f “ v) ⊆ A ∧ ¬ (f “ v) = ∅)))
71		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (x = (f “ v) → (v ≈ x ↔ v ≈ (f “ v)))
72	70, 71	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (x = (f “ v) → (((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) ↔ (((f “ v) ⊆ A ∧ ¬ (f “ v) = ∅) ∧ v ≈ (f “ v))))
73		inteq 1968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (x = (f “ v) → ∩x = ∩(f “ v))
74	73	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (x = (f “ v) → (∩x ∈ A ↔ ∩(f “ v) ∈ A))
75	72, 74	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (x = (f “ v) → ((((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) ↔ ((((f “ v) ⊆ A ∧ ¬ (f “ v) = ∅) ∧ v ≈ (f “ v)) → ∩(f “ v) ∈ A)))
76	66, 75	cla4v 1400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) → ((((f “ v) ⊆ A ∧ ¬ (f “ v) = ∅) ∧ v ≈ (f “ v)) → ∩(f “ v) ∈ A))
77	63, 76	sylan9 359	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f:suc v–1-1-onto→x ∧ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A)) → ((x ⊆ A ∧ ¬ (f “ v) = ∅) → ∩(f “ v) ∈ A))
78		ineq1 1638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (z = ∩(f “ v) → (z ∩ w) = (∩(f “ v) ∩ w))
79	78	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (z = ∩(f “ v) → ((z ∩ w) ∈ A ↔ (∩(f “ v) ∩ w) ∈ A))
80		ineq2 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (w = (f ‘v) → (∩(f “ v) ∩ w) = (∩(f “ v) ∩ (f ‘v)))
81	80	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = (f ‘v) → ((∩(f “ v) ∩ w) ∈ A ↔ (∩(f “ v) ∩ (f ‘v)) ∈ A))
82	79, 81	rcla42v 1404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((∩(f “ v) ∈ A ∧ (f ‘v) ∈ A) → (∩(f “ v) ∩ (f ‘v)) ∈ A))
83	82	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (∩(f “ v) ∈ A → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A)))
84	77, 83	sylan9 359	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((f:suc v–1-1-onto→x ∧ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A)) ∧ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A) → ((x ⊆ A ∧ ¬ (f “ v) = ∅) → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A)))
85	84	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((f:suc v–1-1-onto→x ∧ ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A)) ∧ ∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A) → (x ⊆ A → (¬ (f “ v) = ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))))
86	85	exp31 293	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc v–1-1-onto→x → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (x ⊆ A → (¬ (f “ v) = ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))))))
87	86	com4r 41	. . . . . . . . . . . . . . . . . . . . . . . 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))))))
88	87	imp43 288	. . . . . . . . . . . . . . . . . . . . . . 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)))
89		inteq 1968	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f “ v) = ∅ → ∩(f “ v) = ∩∅)
90		int0 1978	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∩∅ = V
91	89, 90	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f “ v) = ∅ → ∩(f “ v) = V)
92	91	ineq1d 1644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f “ v) = ∅ → (∩(f “ v) ∩ (f ‘v)) = (V ∩ (f ‘v)))
93		ssv 1520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f ‘v) ⊆ V
94		sseqin2 1656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f ‘v) ⊆ V ↔ (V ∩ (f ‘v)) = (f ‘v))
95	93, 94	mpbi 164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (V ∩ (f ‘v)) = (f ‘v)
96	92, 95	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f “ v) = ∅ → (∩(f “ v) ∩ (f ‘v)) = (f ‘v))
97	96	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f “ v) = ∅ → ((∩(f “ v) ∩ (f ‘v)) ∈ A ↔ (f ‘v) ∈ A))
98	97	biimprd 136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f “ v) = ∅ → ((f ‘v) ∈ A → (∩(f “ v) ∩ (f ‘v)) ∈ A))
99	88, 98	pm2.61d2 111	. . . . . . . . . . . . . . . . . . . . . 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))
100	46, 99	mpd 46	. . . . . . . . . . . . . . . . . . . . 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)
101		f1ofn 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc v–1-1-onto→x → f Fn suc v)
102		fnsnfv 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((f Fn suc v ∧ v ∈ suc v) → {(f ‘v)} = (f “ {v}))
103	40, 102	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f Fn suc v → {(f ‘v)} = (f “ {v}))
104	101, 103	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f:suc v–1-1-onto→x → {(f ‘v)} = (f “ {v}))
105	104	uneq2d 1611	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ∪ {(f ‘v)}) = ((f “ v) ∪ (f “ {v})))
106		df-suc 2205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ suc v = (v ∪ {v})
107		imaeq2 2603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (suc v = (v ∪ {v}) → (f “ suc v) = (f “ (v ∪ {v})))
108	106, 107	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f “ suc v) = (f “ (v ∪ {v}))
109		imaun 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f “ (v ∪ {v})) = ((f “ v) ∪ (f “ {v}))
110	108, 109	eqtr2 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f “ v) ∪ (f “ {v})) = (f “ suc v)
111	105, 110	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ∪ {(f ‘v)}) = (f “ suc v))
112		foima 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc v–onto→x → (f “ suc v) = x)
113	37, 112	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc v–1-1-onto→x → (f “ suc v) = x)
114	111, 113	eqtrd 1128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc v–1-1-onto→x → ((f “ v) ∪ {(f ‘v)}) = x)
115	114	inteqd 1970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc v–1-1-onto→x → ∩((f “ v) ∪ {(f ‘v)}) = ∩x)
116		fvex 2838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f ‘v) ∈ V
117	116	intunsn 1993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∩((f “ v) ∪ {(f ‘v)}) = (∩(f “ v) ∩ (f ‘v))
118	115, 117	syl5eqr 1138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f:suc v–1-1-onto→x → (∩(f “ v) ∩ (f ‘v)) = ∩x)
119	118	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc v–1-1-onto→x → ((∩(f “ v) ∩ (f ‘v)) ∈ A ↔ ∩x ∈ A))
120	119	ad2antlr 321	. . . . . . . . . . . . . . . . . . . . 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))
121	100, 120	mpbid 170	. . . . . . . . . . . . . . . . . . . 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)
122	121	exp43 301	. . . . . . . . . . . . . . . . . . 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))))
123	122	19.23adv 954	. . . . . . . . . . . . . . . . . 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))))
124	21	bren 3282	. . . . . . . . . . . . . . . . . 18 ⊢ (suc v ≈ x ↔ ∃f f:suc v–1-1-onto→x)
125	123, 124	syl5ib 181	. . . . . . . . . . . . . . . . 17 ⊢ (x ⊆ A → (suc v ≈ x → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
126	125	imp 277	. . . . . . . . . . . . . . . 16 ⊢ ((x ⊆ A ∧ suc v ≈ x) → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A)))
127	126	adantlr 310	. . . . . . . . . . . . . . 15 ⊢ (((x ⊆ A ∧ ¬ x = ∅) ∧ suc v ≈ x) → (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ v ≈ x) → ∩x ∈ A) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A)))
128	127	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)))
129	33, 34, 128	19.21ad 741	. . . . . . . . . . . . 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)))
130	129	a1i 7	. . . . . . . . . . . 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))))
131	12, 16, 20, 32, 130	finds2 2399	. . . . . . . . . . 11 ⊢ (y ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A)))
132		ax-4 673	. . . . . . . . . . 11 ⊢ (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A) → (((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A))
133	131, 132	syl6 23	. . . . . . . . . 10 ⊢ (y ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (((x ⊆ A ∧ ¬ x = ∅) ∧ y ≈ x) → ∩x ∈ A)))
134	133	exp4a 295	. . . . . . . . 9 ⊢ (y ∈ ω → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((x ⊆ A ∧ ¬ x = ∅) → (y ≈ x → ∩x ∈ A))))
135	134	com24 37	. . . . . . . 8 ⊢ (y ∈ ω → (y ≈ x → ((x ⊆ A ∧ ¬ x = ∅) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
136		visset 1350	. . . . . . . . 9 ⊢ y ∈ V
137	136	ensym 3317	. . . . . . . 8 ⊢ (x ≈ y → y ≈ x)
138	135, 137	syl5 22	. . . . . . 7 ⊢ (y ∈ ω → (x ≈ y → ((x ⊆ A ∧ ¬ x = ∅) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A))))
139	138	r19.23aiv 1284	. . . . . 6 ⊢ (∃y ∈ ω x ≈ y → ((x ⊆ A ∧ ¬ x = ∅) → (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∩x ∈ A)))
140	139	com13 33	. . . . 5 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ((x ⊆ A ∧ ¬ x = ∅) → (∃y ∈ ω x ≈ y → ∩x ∈ A)))
141	140	imp3a 279	. . . 4 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → (((x ⊆ A ∧ ¬ x = ∅) ∧ ∃y ∈ ω x ≈ y) → ∩x ∈ A))
142	141	19.21aiv 943	. . 3 ⊢ (∀z ∈ A ∀w ∈ A (z ∩ w) ∈ A → ∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ ∃y ∈ ω x ≈ y) → ∩x ∈ A))
143		zfpair 1891	. . . . . . . 8 ⊢ {z, w} ∈ V
144		sseq1 1521	. . . . . . . . . . 11 ⊢ (x = {z, w} → (x ⊆ A ↔ {z, w} ⊆ A))
145		cleq1 1107	. . . . . . . . . . . 12 ⊢ (x = {z, w} → (x = ∅ ↔ {z, w} = ∅))
146	145	negbid 463	. . . . . . . . . . 11 ⊢ (x = {z, w} → (¬ x = ∅ ↔ ¬ {z, w} = ∅))
147	144, 146	anbi12d 476	. . . . . . . . . 10 ⊢ (x = {z, w} → ((x ⊆ A ∧ ¬ x = ∅) ↔ ({z, w} ⊆ A ∧ ¬ {z, w} = ∅)))
148		breq1 2065	. . . . . . . . . . 11 ⊢ (x = {z, w} → (x ≈ y ↔ {z, w} ≈ y))
149	148	birexdv 1220	. . . . . . . . . 10 ⊢ (x = {z, w} → (∃y ∈ ω x ≈ y ↔ ∃y ∈ ω {z, w} ≈ y))
150	147, 149	anbi12d 476	. . . . . . . . 9 ⊢ (x = {z, w} → (((x ⊆ A ∧ ¬ x = ∅) ∧ ∃y ∈ ω x ≈ y) ↔ (({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ∧ ∃y ∈ ω {z, w} ≈ y)))
151		inteq 1968	. . . . . . . . . 10 ⊢ (x = {z, w} → ∩x = ∩{z, w})
152	151	eleq1d 1155	. . . . . . . . 9 ⊢ (x = {z, w} → (∩x ∈ A ↔ ∩{z, w} ∈ A))
153	150, 152	imbi12d 474	. . . . . . . 8 ⊢ (x = {z, w} → ((((x ⊆ A ∧ ¬ x = ∅) ∧ ∃y ∈ ω x ≈ y) → ∩x ∈ A) ↔ ((({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ∧ ∃y ∈ ω {z, w} ≈ y) → ∩{z, w} ∈ A)))
154	143, 153	cla4v 1400	. . . . . . 7 ⊢ (∀x(((x ⊆ A ∧ ¬ x = ∅) ∧ ∃y ∈ ω x ≈ y) → ∩x ∈ A) → ((({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ∧ ∃y ∈ ω {z, w} ≈ y) → ∩{z, w} ∈ A))
155		visset 1350	. . . . . . . . . . 11 ⊢ z ∈ V
156	155	prnz 1847	. . . . . . . . . 10 ⊢ ¬ {z, w} = ∅
157	156	biantru 543	. . . . . . . . 9 ⊢ ({z, w} ⊆ A ↔ ({z, w} ⊆ A ∧ ¬ {z, w} = ∅))
158		prfi 3444	. . . . . . . . . 10 ⊢ ∃y ∈ ω {z, w} ≈ y
159	158	biantru 543	. . . . . . . . 9 ⊢ (({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ↔ (({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ∧ ∃y ∈ ω {z, w} ≈ y))
160	157, 159	bitr2 152	. . . . . . . 8 ⊢ ((({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ∧ ∃y ∈ ω {z, w} ≈ y) ↔ {z, w} ⊆ A)
161		visset 1350	. . . . . . . . 9 ⊢ w ∈ V
162	155, 161	prss 1854	. . . . . . . 8 ⊢ ((z ∈ A ∧ w ∈ A) ↔ {z, w} ⊆ A)
163	160, 162	bitr4 154	. . . . . . 7 ⊢ ((({z, w} ⊆ A ∧ ¬ {z, w} = ∅) ∧ ∃y ∈ ω {z, w} ≈ y) ↔ (z ∈ A ∧ w ∈ A))
164	155, 161	intpr 1990