Metamath Proof Explorer

Theorem dffi2

Description: The set of finite intersections is the smallest set that contains A and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion dffi2 ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2 vex ⊢ 𝑡 ∈ V
3 elfi ⊢ ( ( 𝑡 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑡 ∈ ( fi ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑡 = ∩ 𝑥 ) )
4 2 3 mpan ⊢ ( 𝐴 ∈ V → ( 𝑡 ∈ ( fi ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑡 = ∩ 𝑥 ) )
5 4 biimpd ⊢ ( 𝐴 ∈ V → ( 𝑡 ∈ ( fi ‘ 𝐴 ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑡 = ∩ 𝑥 ) )
6 df-rex ⊢ ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑡 = ∩ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) )
7 fiint ⊢ ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝑧 ) )
8 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
9 8 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
10 9 3ad2ant2 ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑥 ⊆ 𝐴 )
11 simp1 ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝐴 ⊆ 𝑧 )
12 10 11 sstrd ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑥 ⊆ 𝑧 )
13 eqvisset ⊢ ( 𝑡 = ∩ 𝑥 → ∩ 𝑥 ∈ V )
14 intex ⊢ ( 𝑥 ≠ ∅ ↔ ∩ 𝑥 ∈ V )
15 13 14 sylibr ⊢ ( 𝑡 = ∩ 𝑥 → 𝑥 ≠ ∅ )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑥 ≠ ∅ )
17 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ Fin )
18 17 3ad2ant2 ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑥 ∈ Fin )
19 12 16 18 3jca ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) )
20 19 3expib ⊢ ( 𝐴 ⊆ 𝑧 → ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ) )
21 pm2.27 ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ( ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝑧 ) → ∩ 𝑥 ∈ 𝑧 ) )
22 20 21 syl6 ⊢ ( 𝐴 ⊆ 𝑧 → ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → ( ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝑧 ) → ∩ 𝑥 ∈ 𝑧 ) ) )
23 eleq1 ⊢ ( 𝑡 = ∩ 𝑥 → ( 𝑡 ∈ 𝑧 ↔ ∩ 𝑥 ∈ 𝑧 ) )
24 23 biimprd ⊢ ( 𝑡 = ∩ 𝑥 → ( ∩ 𝑥 ∈ 𝑧 → 𝑡 ∈ 𝑧 ) )
25 24 adantl ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → ( ∩ 𝑥 ∈ 𝑧 → 𝑡 ∈ 𝑧 ) )
26 25 a1i ⊢ ( 𝐴 ⊆ 𝑧 → ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → ( ∩ 𝑥 ∈ 𝑧 → 𝑡 ∈ 𝑧 ) ) )
27 22 26 syldd ⊢ ( 𝐴 ⊆ 𝑧 → ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → ( ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝑧 ) → 𝑡 ∈ 𝑧 ) ) )
28 27 com23 ⊢ ( 𝐴 ⊆ 𝑧 → ( ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝑧 ) → ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) ) )
29 28 alimdv ⊢ ( 𝐴 ⊆ 𝑧 → ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝑧 ) → ∀ 𝑥 ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) ) )
30 7 29 biimtrid ⊢ ( 𝐴 ⊆ 𝑧 → ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 → ∀ 𝑥 ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) ) )
31 30 imp ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) → ∀ 𝑥 ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) )
32 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) )
33 31 32 sylib ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑡 = ∩ 𝑥 ) → 𝑡 ∈ 𝑧 ) )
34 6 33 biimtrid ⊢ ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) → ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑡 = ∩ 𝑥 → 𝑡 ∈ 𝑧 ) )
35 5 34 sylan9 ⊢ ( ( 𝐴 ∈ V ∧ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) ) → ( 𝑡 ∈ ( fi ‘ 𝐴 ) → 𝑡 ∈ 𝑧 ) )
36 35 ssrdv ⊢ ( ( 𝐴 ∈ V ∧ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) ) → ( fi ‘ 𝐴 ) ⊆ 𝑧 )
37 36 ex ⊢ ( 𝐴 ∈ V → ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) → ( fi ‘ 𝐴 ) ⊆ 𝑧 ) )
38 37 alrimiv ⊢ ( 𝐴 ∈ V → ∀ 𝑧 ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) → ( fi ‘ 𝐴 ) ⊆ 𝑧 ) )
39 ssintab ⊢ ( ( fi ‘ 𝐴 ) ⊆ ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ↔ ∀ 𝑧 ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) → ( fi ‘ 𝐴 ) ⊆ 𝑧 ) )
40 38 39 sylibr ⊢ ( 𝐴 ∈ V → ( fi ‘ 𝐴 ) ⊆ ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } )
41 ssfii ⊢ ( 𝐴 ∈ V → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
42 fiin ⊢ ( ( 𝑥 ∈ ( fi ‘ 𝐴 ) ∧ 𝑦 ∈ ( fi ‘ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) )
43 42 rgen2 ⊢ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 )
44 fvex ⊢ ( fi ‘ 𝐴 ) ∈ V
45 sseq2 ⊢ ( 𝑧 = ( fi ‘ 𝐴 ) → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ ( fi ‘ 𝐴 ) ) )
46 eleq2 ⊢ ( 𝑧 = ( fi ‘ 𝐴 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ) )
47 46 raleqbi1dv ⊢ ( 𝑧 = ( fi ‘ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ) )
48 47 raleqbi1dv ⊢ ( 𝑧 = ( fi ‘ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ) )
49 45 48 anbi12d ⊢ ( 𝑧 = ( fi ‘ 𝐴 ) → ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) ↔ ( 𝐴 ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ) ) )
50 44 49 elab ⊢ ( ( fi ‘ 𝐴 ) ∈ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ↔ ( 𝐴 ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ) )
51 41 43 50 sylanblrc ⊢ ( 𝐴 ∈ V → ( fi ‘ 𝐴 ) ∈ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } )
52 intss1 ⊢ ( ( fi ‘ 𝐴 ) ∈ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } → ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ⊆ ( fi ‘ 𝐴 ) )
53 51 52 syl ⊢ ( 𝐴 ∈ V → ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ⊆ ( fi ‘ 𝐴 ) )
54 40 53 eqssd ⊢ ( 𝐴 ∈ V → ( fi ‘ 𝐴 ) = ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } )
55 1 54 syl ⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } )