Theorem fiintOLD 9395

Description: Obsolete version of fiint 9394 as of 14-Jan-2025. (Contributed by NM, 22-Sep-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
fiintOLD	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))

Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem fiintOLD

Dummy variables 𝑧 𝑤 𝑣 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 9036	. . . . . . 7 ⊢ (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦)
2		ensym 9063	. . . . . . . . 9 ⊢ (𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥)
3		breq1 5169	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥))
4	3	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
5	4	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
6	5	albidv 1919	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
7		breq1 5169	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → (𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥))
8	7	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥)))
9	8	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
10	9	albidv 1919	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
11		breq1 5169	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = suc 𝑣 → (𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥))
12	11	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥)))
13	12	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑦 = suc 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
14	13	albidv 1919	. . . . . . . . . . . . 13 ⊢ (𝑦 = suc 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
15		ensym 9063	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ≈ 𝑥 → 𝑥 ≈ ∅)
16		en0 9078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
17	15, 16	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ≈ 𝑥 → 𝑥 = ∅)
18	17	anim1i 614	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ≈ 𝑥 ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
19	18	ancoms 458	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
20	19	adantll 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21		df-ne 2947	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22		pm3.24 402	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
23	22	pm2.21i 119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → ∩ 𝑥 ∈ 𝐴)
24	21, 23	sylan2b 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)
25	20, 24	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
26	25	ax-gen 1793	. . . . . . . . . . . . . 14 ⊢ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
27	26	a1i 11	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
28		nfv 1913	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴
29		nfa1 2152	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)
30		bren 9013	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑣 ≈ 𝑥 ↔ ∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥)
31		ssel 4002	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ⊆ 𝐴 → ((𝑓‘𝑣) ∈ 𝑥 → (𝑓‘𝑣) ∈ 𝐴))
32		f1of 6862	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣⟶𝑥)
33		vex 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑣 ∈ V
34	33	sucid 6477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑣 ∈ suc 𝑣
35		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:suc 𝑣⟶𝑥 ∧ 𝑣 ∈ suc 𝑣) → (𝑓‘𝑣) ∈ 𝑥)
36	32, 34, 35	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓‘𝑣) ∈ 𝑥)
37	31, 36	impel 505	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) → (𝑓‘𝑣) ∈ 𝐴)
38	37	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴)
39		df-ne 2947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 “ 𝑣) ≠ ∅ ↔ ¬ (𝑓 “ 𝑣) = ∅)
40		imassrn 6100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 “ 𝑣) ⊆ ran 𝑓
41		dff1o2 6867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑥))
42	41	simp3bi 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ran 𝑓 = 𝑥)
43	40, 42	sseqtrid 4061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ⊆ 𝑥)
44		sstr2 4015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓 “ 𝑣) ⊆ 𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
45	43, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴))
46	45	anim1d 610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
47		f1of1 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–1-1→𝑥)
48		vex 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑥 ∈ V
49		sssucid 6475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑣 ⊆ suc 𝑣
50		f1imaen2g 9075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V)) → (𝑓 “ 𝑣) ≈ 𝑣)
51	49, 33, 50	mpanr12 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑣) ≈ 𝑣)
52	47, 48, 51	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ≈ 𝑣)
53	52	ensymd 9065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑣 ≈ (𝑓 “ 𝑣))
54	46, 53	jctird 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
55		vex 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑓 ∈ V
56	55	imaex 7954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 “ 𝑣) ∈ V
57		sseq1 4034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ 𝑣) ⊆ 𝐴))
58		neeq1 3009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ≠ ∅ ↔ (𝑓 “ 𝑣) ≠ ∅))
59	57, 58	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅)))
60		breq2 5170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑣 ≈ 𝑥 ↔ 𝑣 ≈ (𝑓 “ 𝑣)))
61	59, 60	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑓 “ 𝑣) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) ↔ (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣))))
62		inteq 4973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = (𝑓 “ 𝑣) → ∩ 𝑥 = ∩ (𝑓 “ 𝑣))
63	62	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑓 “ 𝑣) → (∩ 𝑥 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑣) ∈ 𝐴))
64	61, 63	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝑓 “ 𝑣) → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴)))
65	56, 64	spcv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
66	54, 65	sylan9 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))
67		ineq1 4234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → (𝑧 ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ 𝑤))
68	67	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = ∩ (𝑓 “ 𝑣) → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴))
69		ineq2 4235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 = (𝑓‘𝑣) → (∩ (𝑓 “ 𝑣) ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)))
70	69	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 = (𝑓‘𝑣) → ((∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
71	68, 70	rspc2v 3646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∩ (𝑓 “ 𝑣) ∈ 𝐴 ∧ (𝑓‘𝑣) ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
72	71	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∩ (𝑓 “ 𝑣) ∈ 𝐴 → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
73	66, 72	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))
74	73	com4r 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))
75	74	exp5c 444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
76	75	com14 96	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))))))
77	76	imp43 427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
78	39, 77	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (¬ (𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))
79		inteq 4973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = ∩ ∅)
80		int0 4986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∩ ∅ = V
81	79, 80	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓 “ 𝑣) = V)
82	81	ineq1d 4240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (V ∩ (𝑓‘𝑣)))
83		ssv 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑣) ⊆ V
84		sseqin2 4244	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓‘𝑣) ⊆ V ↔ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
85	83, 84	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)
86	82, 85	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = (𝑓‘𝑣))
87	86	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 “ 𝑣) = ∅ → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ (𝑓‘𝑣) ∈ 𝐴))
88	87	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
89	78, 88	pm2.61d2 181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))
90	38, 89	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)
91		fvex 6933	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓‘𝑣) ∈ V
92	91	intunsn 5011	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣))
93		f1ofn 6863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓 Fn suc 𝑣)
94		fnsnfv 7001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣) → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
95	93, 34, 94	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → {(𝑓‘𝑣)} = (𝑓 “ {𝑣}))
96	95	uneq2d 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})))
97		df-suc 6401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑣 = (𝑣 ∪ {𝑣})
98	97	imaeq2i 6087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
99		imaundi 6181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣}))
100	98, 99	eqtr2i 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
101	96, 100	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (𝑓 “ suc 𝑣))
102		f1ofo 6869	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–onto→𝑥)
103		foima 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:suc 𝑣–onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
105	101, 104	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = 𝑥)
106	105	inteqd 4975	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ∩ ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ∩ 𝑥)
107	92, 106	eqtr3id 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) = ∩ 𝑥)
108	107	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
109	108	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴))
110	90, 109	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ∩ 𝑥 ∈ 𝐴)
111	110	exp43 436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
112	111	exlimdv 1932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ 𝐴 → (∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
113	30, 112	biimtrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ⊆ 𝐴 → (suc 𝑣 ≈ 𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
114	113	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
115	114	adantlr 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
116	115	com13 88	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
117	28, 29, 116	alrimd 2216	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
118	117	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))))
119	6, 10, 14, 27, 118	finds2 7938	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
120		sp 2184	. . . . . . . . . . . 12 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))
121	119, 120	syl6 35	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))
122	121	exp4a 431	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴))))
123	122	com24 95	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → (𝑦 ≈ 𝑥 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
124	2, 123	syl5 34	. . . . . . . 8 ⊢ (𝑦 ∈ ω → (𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))))
125	124	rexlimiv 3154	. . . . . . 7 ⊢ (∃𝑦 ∈ ω 𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
126	1, 125	sylbi 217	. . . . . 6 ⊢ (𝑥 ∈ Fin → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))
127	126	com13 88	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑥 ∈ Fin → ∩ 𝑥 ∈ 𝐴)))
128	127	impd 410	. . . 4 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
129	128	alrimiv 1926	. . 3 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
130		zfpair2 5448	. . . . . 6 ⊢ {𝑧, 𝑤} ∈ V
131		sseq1 4034	. . . . . . . . 9 ⊢ (𝑥 = {𝑧, 𝑤} → (𝑥 ⊆ 𝐴 ↔ {𝑧, 𝑤} ⊆ 𝐴))
132		neeq1 3009	. . . . . . . . 9 ⊢ (𝑥 = {𝑧, 𝑤} → (𝑥 ≠ ∅ ↔ {𝑧, 𝑤} ≠ ∅))
133	131, 132	anbi12d 631	. . . . . . . 8 ⊢ (𝑥 = {𝑧, 𝑤} → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅)))
134		eleq1 2832	. . . . . . . 8 ⊢ (𝑥 = {𝑧, 𝑤} → (𝑥 ∈ Fin ↔ {𝑧, 𝑤} ∈ Fin))
135	133, 134	anbi12d 631	. . . . . . 7 ⊢ (𝑥 = {𝑧, 𝑤} → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) ↔ (({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin)))
136		inteq 4973	. . . . . . . 8 ⊢ (𝑥 = {𝑧, 𝑤} → ∩ 𝑥 = ∩ {𝑧, 𝑤})
137	136	eleq1d 2829	. . . . . . 7 ⊢ (𝑥 = {𝑧, 𝑤} → (∩ 𝑥 ∈ 𝐴 ↔ ∩ {𝑧, 𝑤} ∈ 𝐴))
138	135, 137	imbi12d 344	. . . . . 6 ⊢ (𝑥 = {𝑧, 𝑤} → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ ((({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin) → ∩ {𝑧, 𝑤} ∈ 𝐴)))
139	130, 138	spcv 3618	. . . . 5 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) → ((({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin) → ∩ {𝑧, 𝑤} ∈ 𝐴))
140		vex 3492	. . . . . . 7 ⊢ 𝑧 ∈ V
141		vex 3492	. . . . . . 7 ⊢ 𝑤 ∈ V
142	140, 141	prss 4845	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ↔ {𝑧, 𝑤} ⊆ 𝐴)
143	140	prnz 4802	. . . . . . 7 ⊢ {𝑧, 𝑤} ≠ ∅
144	143	biantru 529	. . . . . 6 ⊢ ({𝑧, 𝑤} ⊆ 𝐴 ↔ ({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅))
145		prfi 9391	. . . . . . 7 ⊢ {𝑧, 𝑤} ∈ Fin
146	145	biantru 529	. . . . . 6 ⊢ (({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ↔ (({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin))
147	142, 144, 146	3bitrri 298	. . . . 5 ⊢ ((({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴))
148	140, 141	intpr 5006	. . . . . 6 ⊢ ∩ {𝑧, 𝑤} = (𝑧 ∩ 𝑤)
149	148	eleq1i 2835	. . . . 5 ⊢ (∩ {𝑧, 𝑤} ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴)
150	139, 147, 149	3imtr3g 295	. . . 4 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ∩ 𝑤) ∈ 𝐴))
151	150	ralrimivv 3206	. . 3 ⊢ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
152	129, 151	impbii 209	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
153		ineq1 4234	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑦) = (𝑧 ∩ 𝑦))
154	153	eleq1d 2829	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑦) ∈ 𝐴))
155		ineq2 4235	. . . 4 ⊢ (𝑦 = 𝑤 → (𝑧 ∩ 𝑦) = (𝑧 ∩ 𝑤))
156	155	eleq1d 2829	. . 3 ⊢ (𝑦 = 𝑤 → ((𝑧 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴))
157	154, 156	cbvral2vw 3247	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)
158		df-3an 1089	. . . 4 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
159	158	imbi1i 349	. . 3 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
160	159	albii 1817	. 2 ⊢ (∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
161	152, 157, 160	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  {csn 4648  {cpr 4650  ∩ cint 4970   class class class wbr 5166  ^◡ccnv 5699  ran crn 5701   “ cima 5703  suc csuc 6397  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  –1-1→wf1 6570  –onto→wfo 6571  –1-1-onto→wf1o 6572  ‘cfv 6573  ωcom 7903   ≈ cen 9000  Fincfn 9003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-br 5167  df-opab 5229  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-om 7904  df-1o 8522  df-2o 8523  df-er 8763  df-en 9004  df-fin 9007

This theorem is referenced by: (None)