Metamath Proof Explorer

Theorem fin23lem11

Description: Lemma for isfin2-2 . (Contributed by Stefan O'Rear, 31-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Hypotheses fin23lem11.1 ⊢ z = A ∖ x → ψ ↔ χ
fin23lem11.2 ⊢ w = A ∖ v → φ ↔ θ
fin23lem11.3 ⊢ x ⊆ A ∧ v ⊆ A → χ ↔ θ
Assertion fin23lem11 ⊢ B ⊆ 𝒫 A → ∃ x ∈ c ∈ 𝒫 A | A ∖ c ∈ B ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → ∃ z ∈ B ∀ v ∈ B ¬ ψ

Proof

Step Hyp Ref Expression
1 fin23lem11.1 ⊢ z = A ∖ x → ψ ↔ χ
2 fin23lem11.2 ⊢ w = A ∖ v → φ ↔ θ
3 fin23lem11.3 ⊢ x ⊆ A ∧ v ⊆ A → χ ↔ θ
4 difeq2 ⊢ c = x → A ∖ c = A ∖ x
5 4 eleq1d ⊢ c = x → A ∖ c ∈ B ↔ A ∖ x ∈ B
6 5 elrab ⊢ x ∈ c ∈ 𝒫 A | A ∖ c ∈ B ↔ x ∈ 𝒫 A ∧ A ∖ x ∈ B
7 simp2r ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → A ∖ x ∈ B
8 2 notbid ⊢ w = A ∖ v → ¬ φ ↔ ¬ θ
9 simpl3 ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ
10 difeq2 ⊢ c = A ∖ v → A ∖ c = A ∖ A ∖ v
11 10 eleq1d ⊢ c = A ∖ v → A ∖ c ∈ B ↔ A ∖ A ∖ v ∈ B
12 difss ⊢ A ∖ v ⊆ A
13 ssun1 ⊢ A ⊆ A ∪ x
14 undif1 ⊢ A ∖ x ∪ x = A ∪ x
15 13 14 sseqtrri ⊢ A ⊆ A ∖ x ∪ x
16 simpl2r ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ x ∈ B
17 simpl2l ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → x ∈ 𝒫 A
18 unexg ⊢ A ∖ x ∈ B ∧ x ∈ 𝒫 A → A ∖ x ∪ x ∈ V
19 16 17 18 syl2anc ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ x ∪ x ∈ V
20 ssexg ⊢ A ⊆ A ∖ x ∪ x ∧ A ∖ x ∪ x ∈ V → A ∈ V
21 15 19 20 sylancr ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∈ V
22 elpw2g ⊢ A ∈ V → A ∖ v ∈ 𝒫 A ↔ A ∖ v ⊆ A
23 21 22 syl ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ v ∈ 𝒫 A ↔ A ∖ v ⊆ A
24 12 23 mpbiri ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ v ∈ 𝒫 A
25 simpl1 ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → B ⊆ 𝒫 A
26 simpr ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → v ∈ B
27 25 26 sseldd ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → v ∈ 𝒫 A
28 27 elpwid ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → v ⊆ A
29 dfss4 ⊢ v ⊆ A ↔ A ∖ A ∖ v = v
30 28 29 sylib ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ A ∖ v = v
31 30 26 eqeltrd ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ A ∖ v ∈ B
32 11 24 31 elrabd ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → A ∖ v ∈ c ∈ 𝒫 A | A ∖ c ∈ B
33 8 9 32 rspcdva ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → ¬ θ
34 simplrl ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ v ∈ B → x ∈ 𝒫 A
35 34 elpwid ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ v ∈ B → x ⊆ A
36 ssel2 ⊢ B ⊆ 𝒫 A ∧ v ∈ B → v ∈ 𝒫 A
37 36 adantlr ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ v ∈ B → v ∈ 𝒫 A
38 37 elpwid ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ v ∈ B → v ⊆ A
39 35 38 3 syl2anc ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ v ∈ B → χ ↔ θ
40 39 notbid ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ v ∈ B → ¬ χ ↔ ¬ θ
41 40 3adantl3 ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → ¬ χ ↔ ¬ θ
42 33 41 mpbird ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ ∧ v ∈ B → ¬ χ
43 42 ralrimiva ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → ∀ v ∈ B ¬ χ
44 1 notbid ⊢ z = A ∖ x → ¬ ψ ↔ ¬ χ
45 44 ralbidv ⊢ z = A ∖ x → ∀ v ∈ B ¬ ψ ↔ ∀ v ∈ B ¬ χ
46 45 rspcev ⊢ A ∖ x ∈ B ∧ ∀ v ∈ B ¬ χ → ∃ z ∈ B ∀ v ∈ B ¬ ψ
47 7 43 46 syl2anc ⊢ B ⊆ 𝒫 A ∧ x ∈ 𝒫 A ∧ A ∖ x ∈ B ∧ ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → ∃ z ∈ B ∀ v ∈ B ¬ ψ
48 47 3exp ⊢ B ⊆ 𝒫 A → x ∈ 𝒫 A ∧ A ∖ x ∈ B → ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → ∃ z ∈ B ∀ v ∈ B ¬ ψ
49 6 48 syl5bi ⊢ B ⊆ 𝒫 A → x ∈ c ∈ 𝒫 A | A ∖ c ∈ B → ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → ∃ z ∈ B ∀ v ∈ B ¬ ψ
50 49 rexlimdv ⊢ B ⊆ 𝒫 A → ∃ x ∈ c ∈ 𝒫 A | A ∖ c ∈ B ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ φ → ∃ z ∈ B ∀ v ∈ B ¬ ψ