Metamath Proof Explorer

Theorem cmpcovf

Description: Combine cmpcov with ac6sfi to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses iscmp.1 ⊢ 𝑋 = ∪ 𝐽
cmpcovf.2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion cmpcovf ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 iscmp.1 ⊢ 𝑋 = ∪ 𝐽
2 cmpcovf.2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
3 simpl ⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → 𝐽 ∈ Comp )
4 1 cmpcov2 ⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → ∃ 𝑢 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) )
5 elfpw ⊢ ( 𝑢 ∈ ( 𝒫 𝐽 ∩ Fin ) ↔ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) )
6 simplrl ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → 𝑢 ⊆ 𝐽 )
7 velpw ⊢ ( 𝑢 ∈ 𝒫 𝐽 ↔ 𝑢 ⊆ 𝐽 )
8 6 7 sylibr ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → 𝑢 ∈ 𝒫 𝐽 )
9 simplrr ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → 𝑢 ∈ Fin )
10 8 9 elind ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → 𝑢 ∈ ( 𝒫 𝐽 ∩ Fin ) )
11 simprl ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → 𝑋 = ∪ 𝑢 )
12 simprr ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 )
13 2 ac6sfi ⊢ ( ( 𝑢 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑢 𝜓 ) )
14 9 12 13 syl2anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑢 𝜓 ) )
15 unieq ⊢ ( 𝑠 = 𝑢 → ∪ 𝑠 = ∪ 𝑢 )
16 15 eqeq2d ⊢ ( 𝑠 = 𝑢 → ( 𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑢 ) )
17 feq2 ⊢ ( 𝑠 = 𝑢 → ( 𝑓 : 𝑠 ⟶ 𝐴 ↔ 𝑓 : 𝑢 ⟶ 𝐴 ) )
18 raleq ⊢ ( 𝑠 = 𝑢 → ( ∀ 𝑦 ∈ 𝑠 𝜓 ↔ ∀ 𝑦 ∈ 𝑢 𝜓 ) )
19 17 18 anbi12d ⊢ ( 𝑠 = 𝑢 → ( ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ↔ ( 𝑓 : 𝑢 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑢 𝜓 ) ) )
20 19 exbidv ⊢ ( 𝑠 = 𝑢 → ( ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑢 𝜓 ) ) )
21 16 20 anbi12d ⊢ ( 𝑠 = 𝑢 → ( ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) ↔ ( 𝑋 = ∪ 𝑢 ∧ ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑢 𝜓 ) ) ) )
22 21 rspcev ⊢ ( ( 𝑢 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑢 𝜓 ) ) ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) )
23 10 11 14 22 syl12anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) ∧ ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) )
24 23 ex ⊢ ( ( 𝐽 ∈ Comp ∧ ( 𝑢 ⊆ 𝐽 ∧ 𝑢 ∈ Fin ) ) → ( ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) ) )
25 5 24 sylan2b ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑢 ∈ ( 𝒫 𝐽 ∩ Fin ) ) → ( ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) ) )
26 25 rexlimdva ⊢ ( 𝐽 ∈ Comp → ( ∃ 𝑢 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑧 ∈ 𝐴 𝜑 ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) ) )
27 3 4 26 sylc ⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝐴 𝜑 ) ) → ∃ 𝑠 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑠 ∧ ∃ 𝑓 ( 𝑓 : 𝑠 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝑠 𝜓 ) ) )