Theorem ispisys2

Description: The property of being a pi-system, expanded version. Pi-systems are closed under finite intersections. (Contributed by Thierry Arnoux, 13-Jun-2020)

	Ref	Expression
Hypothesis	ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
Assertion	ispisys2	⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2	1	ispisys	⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) )
3		dfss3	⊢ ( ( fi ‘ 𝑆 ) ⊆ 𝑆 ↔ ∀ 𝑦 ∈ ( fi ‘ 𝑆 ) 𝑦 ∈ 𝑆 )
4		elex	⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → 𝑆 ∈ V )
5	4	adantr	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑆 ∈ V )
6		eldifsn	⊢ ( 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
7	6	bilani	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
8	7	simpld	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) )
9	8	elin1d	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ 𝒫 𝑆 )
10	9	elpwid	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ⊆ 𝑆 )
11	7	simprd	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ≠ ∅ )
12	8	elin2d	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ Fin )
13		elfir	⊢ ( ( 𝑆 ∈ V ∧ ( 𝑥 ⊆ 𝑆 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ) → ∩ 𝑥 ∈ ( fi ‘ 𝑆 ) )
14	5 10 11 12 13	syl13anc	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑥 ∈ ( fi ‘ 𝑆 ) )
15		elfi2	⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → ( 𝑦 ∈ ( fi ‘ 𝑆 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) 𝑦 = ∩ 𝑥 ) )
16	15	biimpa	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑦 ∈ ( fi ‘ 𝑆 ) ) → ∃ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) 𝑦 = ∩ 𝑥 )
17		simpr	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 = ∩ 𝑥 )
18	17	eleq1d	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑦 = ∩ 𝑥 ) → ( 𝑦 ∈ 𝑆 ↔ ∩ 𝑥 ∈ 𝑆 ) )
19	14 16 18	ralxfrd	⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → ( ∀ 𝑦 ∈ ( fi ‘ 𝑆 ) 𝑦 ∈ 𝑆 ↔ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
20	3 19	bitrid	⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → ( ( fi ‘ 𝑆 ) ⊆ 𝑆 ↔ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
21	20	pm5.32i	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
22	2 21	bitri	⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )