Theorem superficl

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

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

Proof

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