Metamath Proof Explorer

Theorem cmpcov2

Description: Rewrite cmpcov for the cover { y e. J | ph } . (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis iscmp.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cmpcov2 ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) )

Proof

Step Hyp Ref Expression
1 iscmp.1 ⊢ 𝑋 = ∪ 𝐽
2 dfss3 ⊢ ( 𝑋 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } )
3 elunirab ⊢ ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
4 3 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
5 2 4 sylbbr ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → 𝑋 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } )
6 ssrab2 ⊢ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ⊆ 𝐽
7 6 unissi ⊢ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ⊆ ∪ 𝐽
8 7 1 sseqtrri ⊢ ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ⊆ 𝑋
9 8 a1i ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ⊆ 𝑋 )
10 5 9 eqssd ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → 𝑋 = ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } )
11 1 cmpcov ⊢ ( ( 𝐽 ∈ Comp ∧ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ⊆ 𝐽 ∧ 𝑋 = ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ) → ∃ 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) 𝑋 = ∪ 𝑠 )
12 6 11 mp3an2 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑋 = ∪ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ) → ∃ 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) 𝑋 = ∪ 𝑠 )
13 10 12 sylan2 ⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ∃ 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) 𝑋 = ∪ 𝑠 )
14 ssrab ⊢ ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ↔ ( 𝑠 ⊆ 𝐽 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) )
15 14 anbi1i ⊢ ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑠 ⊆ 𝐽 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ∧ 𝑋 = ∪ 𝑠 ) )
16 an32 ⊢ ( ( ( 𝑠 ⊆ 𝐽 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ∧ 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑠 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑠 ) ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) )
17 anass ⊢ ( ( ( 𝑠 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑠 ) ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ↔ ( 𝑠 ⊆ 𝐽 ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) )
18 15 16 17 3bitri ⊢ ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑋 = ∪ 𝑠 ) ↔ ( 𝑠 ⊆ 𝐽 ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) )
19 18 anbi1i ⊢ ( ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑋 = ∪ 𝑠 ) ∧ 𝑠 ∈ Fin ) ↔ ( ( 𝑠 ⊆ 𝐽 ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) ∧ 𝑠 ∈ Fin ) )
20 an32 ⊢ ( ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑠 ∈ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑋 = ∪ 𝑠 ) ∧ 𝑠 ∈ Fin ) )
21 an32 ⊢ ( ( ( 𝑠 ⊆ 𝐽 ∧ 𝑠 ∈ Fin ) ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) ↔ ( ( 𝑠 ⊆ 𝐽 ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) ∧ 𝑠 ∈ Fin ) )
22 19 20 21 3bitr4i ⊢ ( ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑠 ∈ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑠 ⊆ 𝐽 ∧ 𝑠 ∈ Fin ) ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) )
23 elfpw ⊢ ( 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) ↔ ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑠 ∈ Fin ) )
24 23 anbi1i ⊢ ( ( 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑠 ⊆ { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∧ 𝑠 ∈ Fin ) ∧ 𝑋 = ∪ 𝑠 ) )
25 elfpw ⊢ ( 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ↔ ( 𝑠 ⊆ 𝐽 ∧ 𝑠 ∈ Fin ) )
26 25 anbi1i ⊢ ( ( 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) ↔ ( ( 𝑠 ⊆ 𝐽 ∧ 𝑠 ∈ Fin ) ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) )
27 22 24 26 3bitr4i ⊢ ( ( 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ↔ ( 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) ) )
28 27 rexbii2 ⊢ ( ∃ 𝑠 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ 𝜑 } ∩ Fin ) 𝑋 = ∪ 𝑠 ↔ ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) )
29 13 28 sylib ⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑦 ∈ 𝑠 𝜑 ) )