This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑧 = ( 𝐴 ∖ 𝑥 ) → ( 𝜓 ↔ 𝜒 ) )
fin23lem11.2 ⊢ ( 𝑤 = ( 𝐴 ∖ 𝑣 ) → ( 𝜑 ↔ 𝜃 ) )
fin23lem11.3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) )
Assertion fin23lem11 ( 𝐵 ⊆ 𝒫 𝐴 → ( ∃ 𝑥 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 fin23lem11.1 ⊢ ( 𝑧 = ( 𝐴 ∖ 𝑥 ) → ( 𝜓 ↔ 𝜒 ) )
2 fin23lem11.2 ⊢ ( 𝑤 = ( 𝐴 ∖ 𝑣 ) → ( 𝜑 ↔ 𝜃 ) )
3 fin23lem11.3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) )
4 difeq2 ⊢ ( 𝑐 = 𝑥 → ( 𝐴 ∖ 𝑐 ) = ( 𝐴 ∖ 𝑥 ) )
5 4 eleq1d ⊢ ( 𝑐 = 𝑥 → ( ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 ↔ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) )
6 5 elrab ⊢ ( 𝑥 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) )
7 simp2r ⊢ ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 )
8 2 notbid ⊢ ( 𝑤 = ( 𝐴 ∖ 𝑣 ) → ( ¬ 𝜑 ↔ ¬ 𝜃 ) )
9 simpl3 ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 )
10 difeq2 ⊢ ( 𝑐 = ( 𝐴 ∖ 𝑣 ) → ( 𝐴 ∖ 𝑐 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝑣 ) ) )
11 10 eleq1d ⊢ ( 𝑐 = ( 𝐴 ∖ 𝑣 ) → ( ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑣 ) ) ∈ 𝐵 ) )
12 difss ⊢ ( 𝐴 ∖ 𝑣 ) ⊆ 𝐴
13 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝑥 )
14 undif1 ⊢ ( ( 𝐴 ∖ 𝑥 ) ∪ 𝑥 ) = ( 𝐴 ∪ 𝑥 )
15 13 14 sseqtrri ⊢ 𝐴 ⊆ ( ( 𝐴 ∖ 𝑥 ) ∪ 𝑥 )
16 simpl2r ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 )
17 simpl2l ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑥 ∈ 𝒫 𝐴 )
18 unexg ⊢ ( ( ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( ( 𝐴 ∖ 𝑥 ) ∪ 𝑥 ) ∈ V )
19 16 17 18 syl2anc ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝐴 ∖ 𝑥 ) ∪ 𝑥 ) ∈ V )
20 ssexg ⊢ ( ( 𝐴 ⊆ ( ( 𝐴 ∖ 𝑥 ) ∪ 𝑥 ) ∧ ( ( 𝐴 ∖ 𝑥 ) ∪ 𝑥 ) ∈ V ) → 𝐴 ∈ V )
21 15 19 20 sylancr ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐴 ∈ V )
22 elpw2g ⊢ ( 𝐴 ∈ V → ( ( 𝐴 ∖ 𝑣 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑣 ) ⊆ 𝐴 ) )
23 21 22 syl ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝐴 ∖ 𝑣 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑣 ) ⊆ 𝐴 ) )
24 12 23 mpbiri ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝐴 ∖ 𝑣 ) ∈ 𝒫 𝐴 )
25 simpl1 ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐵 ⊆ 𝒫 𝐴 )
26 simpr ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
27 25 26 sseldd ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝒫 𝐴 )
28 27 elpwid ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ⊆ 𝐴 )
29 dfss4 ⊢ ( 𝑣 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑣 ) ) = 𝑣 )
30 28 29 sylib ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑣 ) ) = 𝑣 )
31 30 26 eqeltrd ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑣 ) ) ∈ 𝐵 )
32 11 24 31 elrabd ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝐴 ∖ 𝑣 ) ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } )
33 8 9 32 rspcdva ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ¬ 𝜃 )
34 simplrl ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝑥 ∈ 𝒫 𝐴 )
35 34 elpwid ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝑥 ⊆ 𝐴 )
36 ssel2 ⊢ ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝒫 𝐴 )
37 36 adantlr ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝒫 𝐴 )
38 37 elpwid ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ⊆ 𝐴 )
39 35 38 3 syl2anc ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
40 39 notbid ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( ¬ 𝜒 ↔ ¬ 𝜃 ) )
41 40 3adantl3 ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ( ¬ 𝜒 ↔ ¬ 𝜃 ) )
42 33 41 mpbird ⊢ ( ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) ∧ 𝑣 ∈ 𝐵 ) → ¬ 𝜒 )
43 42 ralrimiva ⊢ ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) → ∀ 𝑣 ∈ 𝐵 ¬ 𝜒 )
44 1 notbid ⊢ ( 𝑧 = ( 𝐴 ∖ 𝑥 ) → ( ¬ 𝜓 ↔ ¬ 𝜒 ) )
45 44 ralbidv ⊢ ( 𝑧 = ( 𝐴 ∖ 𝑥 ) → ( ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ↔ ∀ 𝑣 ∈ 𝐵 ¬ 𝜒 ) )
46 45 rspcev ⊢ ( ( ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑣 ∈ 𝐵 ¬ 𝜒 ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 )
47 7 43 46 syl2anc ⊢ ( ( 𝐵 ⊆ 𝒫 𝐴 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 )
48 47 3exp ⊢ ( 𝐵 ⊆ 𝒫 𝐴 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) → ( ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ) ) )
49 6 48 biimtrid ⊢ ( 𝐵 ⊆ 𝒫 𝐴 → ( 𝑥 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } → ( ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ) ) )
50 49 rexlimdv ⊢ ( 𝐵 ⊆ 𝒫 𝐴 → ( ∃ 𝑥 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ) )