Theorem ssficl

Description: The class of all subsets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020) (Proof shortened by RP, 3-Jan-2020)

	Ref	Expression
Hypothesis	ssficl.a	⊢ 𝐴 = { 𝑧 ∣ 𝑧 ⊆ 𝐵 }
Assertion	ssficl	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssficl.a	⊢ 𝐴 = { 𝑧 ∣ 𝑧 ⊆ 𝐵 }
2		vex	⊢ 𝑥 ∈ V
3	2	inex1	⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
4		sseq1	⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ⊆ 𝐵 ↔ ( 𝑥 ∩ 𝑦 ) ⊆ 𝐵 ) )
5		sseq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ⊆ 𝐵 ↔ 𝑥 ⊆ 𝐵 ) )
6		sseq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵 ) )
7		ssinss1	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ∩ 𝑦 ) ⊆ 𝐵 )
8	7	adantr	⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝐵 )
9	1 3 4 5 6 8	cllem0	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴