This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inficl

Description: A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion inficl ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ↔ ( fi ‘ 𝐴 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssfii ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
2 eqimss2 ⊢ ( 𝑧 = 𝐴 → 𝐴 ⊆ 𝑧 )
3 2 biantrurd ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) ) )
4 eleq2 ⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
5 4 raleqbi1dv ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
6 5 raleqbi1dv ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
7 3 6 bitr3d ⊢ ( 𝑧 = 𝐴 → ( ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
8 7 elabg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
9 intss1 ⊢ ( 𝐴 ∈ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } → ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ⊆ 𝐴 )
10 8 9 biimtrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 → ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ⊆ 𝐴 ) )
11 dffi2 ⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } )
12 11 sseq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( fi ‘ 𝐴 ) ⊆ 𝐴 ↔ ∩ { 𝑧 ∣ ( 𝐴 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ∈ 𝑧 ) } ⊆ 𝐴 ) )
13 10 12 sylibrd ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 → ( fi ‘ 𝐴 ) ⊆ 𝐴 ) )
14 eqss ⊢ ( ( fi ‘ 𝐴 ) = 𝐴 ↔ ( ( fi ‘ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( fi ‘ 𝐴 ) ) )
15 14 simplbi2com ⊢ ( 𝐴 ⊆ ( fi ‘ 𝐴 ) → ( ( fi ‘ 𝐴 ) ⊆ 𝐴 → ( fi ‘ 𝐴 ) = 𝐴 ) )
16 1 13 15 sylsyld ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 → ( fi ‘ 𝐴 ) = 𝐴 ) )
17 fiin ⊢ ( ( 𝑥 ∈ ( fi ‘ 𝐴 ) ∧ 𝑦 ∈ ( fi ‘ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) )
18 17 rgen2 ⊢ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 )
19 eleq2 ⊢ ( ( fi ‘ 𝐴 ) = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ↔ ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
20 19 raleqbi1dv ⊢ ( ( fi ‘ 𝐴 ) = 𝐴 → ( ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
21 20 raleqbi1dv ⊢ ( ( fi ‘ 𝐴 ) = 𝐴 → ( ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ) )
22 18 21 mpbii ⊢ ( ( fi ‘ 𝐴 ) = 𝐴 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 )
23 16 22 impbid1 ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴 ↔ ( fi ‘ 𝐴 ) = 𝐴 ) )