Metamath Proof Explorer

Theorem fiint

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 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. (Contributed by NM, 22-Sep-2002)

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

Proof

Step Hyp Ref Expression
1 isfi ⊢ ( 𝑥 ∈ Fin ↔ ∃ 𝑦 ∈ ω 𝑥 ≈ 𝑦 )
2 ensym ⊢ ( 𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥 )
3 breq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥 ) )
4 3 anbi2d ⊢ ( 𝑦 = ∅ → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) ) )
5 4 imbi1d ⊢ ( 𝑦 = ∅ → ( ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
6 5 albidv ⊢ ( 𝑦 = ∅ → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
7 breq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥 ) )
8 7 anbi2d ⊢ ( 𝑦 = 𝑣 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) ) )
9 8 imbi1d ⊢ ( 𝑦 = 𝑣 → ( ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
10 9 albidv ⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
11 breq1 ⊢ ( 𝑦 = suc 𝑣 → ( 𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥 ) )
12 11 anbi2d ⊢ ( 𝑦 = suc 𝑣 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) ) )
13 12 imbi1d ⊢ ( 𝑦 = suc 𝑣 → ( ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
14 13 albidv ⊢ ( 𝑦 = suc 𝑣 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
15 ensym ⊢ ( ∅ ≈ 𝑥 → 𝑥 ≈ ∅ )
16 en0 ⊢ ( 𝑥 ≈ ∅ ↔ 𝑥 = ∅ )
17 15 16 sylib ⊢ ( ∅ ≈ 𝑥 → 𝑥 = ∅ )
18 17 anim1i ⊢ ( ( ∅ ≈ 𝑥 ∧ 𝑥 ≠ ∅ ) → ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) )
19 18 ancoms ⊢ ( ( 𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥 ) → ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) )
20 19 adantll ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) )
21 df-ne ⊢ ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅ )
22 pm3.24 ⊢ ¬ ( 𝑥 = ∅ ∧ ¬ 𝑥 = ∅ )
23 22 pm2.21i ⊢ ( ( 𝑥 = ∅ ∧ ¬ 𝑥 = ∅ ) → ∩ 𝑥 ∈ 𝐴 )
24 21 23 sylan2b ⊢ ( ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 )
25 20 24 syl ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 )
26 25 ax-gen ⊢ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 )
27 26 a1i ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) )
28 nfv ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴
29 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 )
30 bren ⊢ ( suc 𝑣 ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 )
31 ssel ⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑥 → ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 ) )
32 f1of ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → 𝑓 : suc 𝑣 ⟶ 𝑥 )
33 vex ⊢ 𝑣 ∈ V
34 33 sucid ⊢ 𝑣 ∈ suc 𝑣
35 ffvelrn ⊢ ( ( 𝑓 : suc 𝑣 ⟶ 𝑥 ∧ 𝑣 ∈ suc 𝑣 ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝑥 )
36 32 34 35 sylancl ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( 𝑓 ‘ 𝑣 ) ∈ 𝑥 )
37 31 36 impel ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 )
38 37 adantr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 )
39 df-ne ⊢ ( ( 𝑓 “ 𝑣 ) ≠ ∅ ↔ ¬ ( 𝑓 “ 𝑣 ) = ∅ )
40 imassrn ⊢ ( 𝑓 “ 𝑣 ) ⊆ ran 𝑓
41 dff1o2 ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ↔ ( 𝑓 Fn suc 𝑣 ∧ Fun ◡ 𝑓 ∧ ran 𝑓 = 𝑥 ) )
42 41 simp3bi ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ran 𝑓 = 𝑥 )
43 40 42 sseqtrid ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( 𝑓 “ 𝑣 ) ⊆ 𝑥 )
44 sstr2 ⊢ ( ( 𝑓 “ 𝑣 ) ⊆ 𝑥 → ( 𝑥 ⊆ 𝐴 → ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ) )
45 43 44 syl ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( 𝑥 ⊆ 𝐴 → ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ) )
46 45 anim1d ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) → ( ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) ) )
47 f1of1 ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → 𝑓 : suc 𝑣 –1-1→ 𝑥 )
48 vex ⊢ 𝑥 ∈ V
49 sssucid ⊢ 𝑣 ⊆ suc 𝑣
50 f1imaen2g ⊢ ( ( ( 𝑓 : suc 𝑣 –1-1→ 𝑥 ∧ 𝑥 ∈ V ) ∧ ( 𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V ) ) → ( 𝑓 “ 𝑣 ) ≈ 𝑣 )
51 49 33 50 mpanr12 ⊢ ( ( 𝑓 : suc 𝑣 –1-1→ 𝑥 ∧ 𝑥 ∈ V ) → ( 𝑓 “ 𝑣 ) ≈ 𝑣 )
52 47 48 51 sylancl ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( 𝑓 “ 𝑣 ) ≈ 𝑣 )
53 52 ensymd ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → 𝑣 ≈ ( 𝑓 “ 𝑣 ) )
54 46 53 jctird ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) → ( ( ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓 “ 𝑣 ) ) ) )
55 vex ⊢ 𝑓 ∈ V
56 55 imaex ⊢ ( 𝑓 “ 𝑣 ) ∈ V
57 sseq1 ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ) )
58 neeq1 ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( 𝑥 ≠ ∅ ↔ ( 𝑓 “ 𝑣 ) ≠ ∅ ) )
59 57 58 anbi12d ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ↔ ( ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) ) )
60 breq2 ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( 𝑣 ≈ 𝑥 ↔ 𝑣 ≈ ( 𝑓 “ 𝑣 ) ) )
61 59 60 anbi12d ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) ↔ ( ( ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓 “ 𝑣 ) ) ) )
62 inteq ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ∩ 𝑥 = ∩ ( 𝑓 “ 𝑣 ) )
63 62 eleq1d ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( ∩ 𝑥 ∈ 𝐴 ↔ ∩ ( 𝑓 “ 𝑣 ) ∈ 𝐴 ) )
64 61 63 imbi12d ⊢ ( 𝑥 = ( 𝑓 “ 𝑣 ) → ( ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ( ( ( ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓 “ 𝑣 ) ) → ∩ ( 𝑓 “ 𝑣 ) ∈ 𝐴 ) ) )
65 56 64 spcv ⊢ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝑓 “ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓 “ 𝑣 ) ) → ∩ ( 𝑓 “ 𝑣 ) ∈ 𝐴 ) )
66 54 65 sylan9 ⊢ ( ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ∧ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) → ∩ ( 𝑓 “ 𝑣 ) ∈ 𝐴 ) )
67 ineq1 ⊢ ( 𝑧 = ∩ ( 𝑓 “ 𝑣 ) → ( 𝑧 ∩ 𝑤 ) = ( ∩ ( 𝑓 “ 𝑣 ) ∩ 𝑤 ) )
68 67 eleq1d ⊢ ( 𝑧 = ∩ ( 𝑓 “ 𝑣 ) → ( ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ( ∩ ( 𝑓 “ 𝑣 ) ∩ 𝑤 ) ∈ 𝐴 ) )
69 ineq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑣 ) → ( ∩ ( 𝑓 “ 𝑣 ) ∩ 𝑤 ) = ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) )
70 69 eleq1d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑣 ) → ( ( ∩ ( 𝑓 “ 𝑣 ) ∩ 𝑤 ) ∈ 𝐴 ↔ ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) )
71 68 70 rspc2v ⊢ ( ( ∩ ( 𝑓 “ 𝑣 ) ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) )
72 71 ex ⊢ ( ∩ ( 𝑓 “ 𝑣 ) ∈ 𝐴 → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) )
73 66 72 syl6 ⊢ ( ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ∧ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) ) )
74 73 com4r ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ∧ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑓 “ 𝑣 ) ≠ ∅ ) → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) ) )
75 74 exp5c ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( 𝑥 ⊆ 𝐴 → ( ( 𝑓 “ 𝑣 ) ≠ ∅ → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) ) ) ) )
76 75 com14 ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ( 𝑓 “ 𝑣 ) ≠ ∅ → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) ) ) ) )
77 76 imp43 ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ( ( 𝑓 “ 𝑣 ) ≠ ∅ → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) )
78 39 77 syl5bir ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ( ¬ ( 𝑓 “ 𝑣 ) = ∅ → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) ) )
79 inteq ⊢ ( ( 𝑓 “ 𝑣 ) = ∅ → ∩ ( 𝑓 “ 𝑣 ) = ∩ ∅ )
80 int0 ⊢ ∩ ∅ = V
81 79 80 eqtrdi ⊢ ( ( 𝑓 “ 𝑣 ) = ∅ → ∩ ( 𝑓 “ 𝑣 ) = V )
82 81 ineq1d ⊢ ( ( 𝑓 “ 𝑣 ) = ∅ → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) = ( V ∩ ( 𝑓 ‘ 𝑣 ) ) )
83 ssv ⊢ ( 𝑓 ‘ 𝑣 ) ⊆ V
84 sseqin2 ⊢ ( ( 𝑓 ‘ 𝑣 ) ⊆ V ↔ ( V ∩ ( 𝑓 ‘ 𝑣 ) ) = ( 𝑓 ‘ 𝑣 ) )
85 83 84 mpbi ⊢ ( V ∩ ( 𝑓 ‘ 𝑣 ) ) = ( 𝑓 ‘ 𝑣 )
86 82 85 eqtrdi ⊢ ( ( 𝑓 “ 𝑣 ) = ∅ → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) = ( 𝑓 ‘ 𝑣 ) )
87 86 eleq1d ⊢ ( ( 𝑓 “ 𝑣 ) = ∅ → ( ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ↔ ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 ) )
88 87 biimprd ⊢ ( ( 𝑓 “ 𝑣 ) = ∅ → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) )
89 78 88 pm2.61d2 ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐴 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ) )
90 38 89 mpd ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 )
91 fvex ⊢ ( 𝑓 ‘ 𝑣 ) ∈ V
92 91 intunsn ⊢ ∩ ( ( 𝑓 “ 𝑣 ) ∪ { ( 𝑓 ‘ 𝑣 ) } ) = ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) )
93 f1ofn ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → 𝑓 Fn suc 𝑣 )
94 fnsnfv ⊢ ( ( 𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣 ) → { ( 𝑓 ‘ 𝑣 ) } = ( 𝑓 “ { 𝑣 } ) )
95 93 34 94 sylancl ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → { ( 𝑓 ‘ 𝑣 ) } = ( 𝑓 “ { 𝑣 } ) )
96 95 uneq2d ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ( 𝑓 “ 𝑣 ) ∪ { ( 𝑓 ‘ 𝑣 ) } ) = ( ( 𝑓 “ 𝑣 ) ∪ ( 𝑓 “ { 𝑣 } ) ) )
97 df-suc ⊢ suc 𝑣 = ( 𝑣 ∪ { 𝑣 } )
98 97 imaeq2i ⊢ ( 𝑓 “ suc 𝑣 ) = ( 𝑓 “ ( 𝑣 ∪ { 𝑣 } ) )
99 imaundi ⊢ ( 𝑓 “ ( 𝑣 ∪ { 𝑣 } ) ) = ( ( 𝑓 “ 𝑣 ) ∪ ( 𝑓 “ { 𝑣 } ) )
100 98 99 eqtr2i ⊢ ( ( 𝑓 “ 𝑣 ) ∪ ( 𝑓 “ { 𝑣 } ) ) = ( 𝑓 “ suc 𝑣 )
101 96 100 eqtrdi ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ( 𝑓 “ 𝑣 ) ∪ { ( 𝑓 ‘ 𝑣 ) } ) = ( 𝑓 “ suc 𝑣 ) )
102 f1ofo ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → 𝑓 : suc 𝑣 –onto→ 𝑥 )
103 foima ⊢ ( 𝑓 : suc 𝑣 –onto→ 𝑥 → ( 𝑓 “ suc 𝑣 ) = 𝑥 )
104 102 103 syl ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( 𝑓 “ suc 𝑣 ) = 𝑥 )
105 101 104 eqtrd ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ( 𝑓 “ 𝑣 ) ∪ { ( 𝑓 ‘ 𝑣 ) } ) = 𝑥 )
106 105 inteqd ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ∩ ( ( 𝑓 “ 𝑣 ) ∪ { ( 𝑓 ‘ 𝑣 ) } ) = ∩ 𝑥 )
107 92 106 eqtr3id ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) = ∩ 𝑥 )
108 107 eleq1d ⊢ ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴 ) )
109 108 ad2antlr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ( ( ∩ ( 𝑓 “ 𝑣 ) ∩ ( 𝑓 ‘ 𝑣 ) ) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴 ) )
110 90 109 mpbid ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) ) → ∩ 𝑥 ∈ 𝐴 )
111 110 exp43 ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) ) )
112 111 exlimdv ⊢ ( 𝑥 ⊆ 𝐴 → ( ∃ 𝑓 𝑓 : suc 𝑣 –1-1-onto→ 𝑥 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) ) )
113 30 112 syl5bi ⊢ ( 𝑥 ⊆ 𝐴 → ( suc 𝑣 ≈ 𝑥 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) ) )
114 113 imp ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥 ) → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) )
115 114 adantlr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) )
116 115 com13 ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
117 28 29 116 alrimd ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
118 117 a1i ⊢ ( 𝑣 ∈ ω → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ suc 𝑣 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) ) )
119 6 10 14 27 118 finds2 ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
120 sp ⊢ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) )
121 119 120 syl6 ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ≈ 𝑥 ) → ∩ 𝑥 ∈ 𝐴 ) ) )
122 121 exp4a ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴 ) ) ) )
123 122 com24 ⊢ ( 𝑦 ∈ ω → ( 𝑦 ≈ 𝑥 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) ) )
124 2 123 syl5 ⊢ ( 𝑦 ∈ ω → ( 𝑥 ≈ 𝑦 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) ) )
125 124 rexlimiv ⊢ ( ∃ 𝑦 ∈ ω 𝑥 ≈ 𝑦 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) )
126 1 125 sylbi ⊢ ( 𝑥 ∈ Fin → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ) ) )
127 126 com13 ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝑥 ∈ Fin → ∩ 𝑥 ∈ 𝐴 ) ) )
128 127 impd ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) )
129 128 alrimiv ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 → ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) )
130 zfpair2 ⊢ { 𝑧 , 𝑤 } ∈ V
131 sseq1 ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥 ⊆ 𝐴 ↔ { 𝑧 , 𝑤 } ⊆ 𝐴 ) )
132 neeq1 ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥 ≠ ∅ ↔ { 𝑧 , 𝑤 } ≠ ∅ ) )
133 131 132 anbi12d ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ↔ ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ) )
134 eleq1 ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥 ∈ Fin ↔ { 𝑧 , 𝑤 } ∈ Fin ) )
135 133 134 anbi12d ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) ↔ ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) ) )
136 inteq ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ∩ 𝑥 = ∩ { 𝑧 , 𝑤 } )
137 136 eleq1d ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( ∩ 𝑥 ∈ 𝐴 ↔ ∩ { 𝑧 , 𝑤 } ∈ 𝐴 ) )
138 135 137 imbi12d ⊢ ( 𝑥 = { 𝑧 , 𝑤 } → ( ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ( ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) → ∩ { 𝑧 , 𝑤 } ∈ 𝐴 ) ) )
139 130 138 spcv ⊢ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) → ( ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) → ∩ { 𝑧 , 𝑤 } ∈ 𝐴 ) )
140 vex ⊢ 𝑧 ∈ V
141 vex ⊢ 𝑤 ∈ V
142 140 141 prss ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ↔ { 𝑧 , 𝑤 } ⊆ 𝐴 )
143 140 prnz ⊢ { 𝑧 , 𝑤 } ≠ ∅
144 143 biantru ⊢ ( { 𝑧 , 𝑤 } ⊆ 𝐴 ↔ ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) )
145 prfi ⊢ { 𝑧 , 𝑤 } ∈ Fin
146 145 biantru ⊢ ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ↔ ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) )
147 142 144 146 3bitrri ⊢ ( ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
148 140 141 intpr ⊢ ∩ { 𝑧 , 𝑤 } = ( 𝑧 ∩ 𝑤 )
149 148 eleq1i ⊢ ( ∩ { 𝑧 , 𝑤 } ∈ 𝐴 ↔ ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
150 139 147 149 3imtr3g ⊢ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) )
151 150 ralrimivv ⊢ ( ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
152 129 151 impbii ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) )
153 ineq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑦 ) )
154 153 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ↔ ( 𝑧 ∩ 𝑦 ) ∈ 𝐴 ) )
155 ineq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑤 ) )
156 155 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ∩ 𝑦 ) ∈ 𝐴 ↔ ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ) )
157 154 156 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
158 df-3an ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) )
159 158 imbi1i ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) )
160 159 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) )
161 152 157 160 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐴 ) )