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 biimtrid ⊢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¬ψ