Metamath Proof Explorer

Theorem cplem2

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003)

Ref Expression
Hypothesis cplem2.1 ⊢A∈V
Assertion cplem2 ⊢∃y∀x∈AB≠∅→B∩y≠∅

Proof

Step Hyp Ref Expression
1 cplem2.1 ⊢A∈V
2 scottex ⊢z∈B|∀w∈Brank⁡z⊆rank⁡w∈V
3 1 2 iunex ⊢⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w∈V
4 nfiu1 ⊢Ⅎ_x⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w
5 4 nfeq2 ⊢Ⅎxy=⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w
6 ineq2 ⊢y=⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w→B∩y=B∩⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w
7 6 neeq1d ⊢y=⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w→B∩y≠∅↔B∩⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w≠∅
8 7 imbi2d ⊢y=⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w→B≠∅→B∩y≠∅↔B≠∅→B∩⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w≠∅
9 5 8 ralbid ⊢y=⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w→∀x∈AB≠∅→B∩y≠∅↔∀x∈AB≠∅→B∩⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w≠∅
10 eqid ⊢z∈B|∀w∈Brank⁡z⊆rank⁡w=z∈B|∀w∈Brank⁡z⊆rank⁡w
11 eqid ⊢⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w=⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w
12 10 11 cplem1 ⊢∀x∈AB≠∅→B∩⋃x∈Az∈B|∀w∈Brank⁡z⊆rank⁡w≠∅
13 3 9 12 ceqsexv2d ⊢∃y∀x∈AB≠∅→B∩y≠∅