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	syl5bi	⊢ ( 𝐵 ⊆ 𝒫 𝐴 → ( 𝑥 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } → ( ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ) ) )
50	49	rexlimdv	⊢ ( 𝐵 ⊆ 𝒫 𝐴 → ( ∃ 𝑥 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝜓 ) )