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) Use a separate setvar for the right-hand side and avoid ax-pow . (Revised by BTernaryTau, 14-Jan-2025)

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

Proof

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