Theorem fin23lem11 9425

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

Hypotheses

Ref	Expression
fin23lem11.1	⊢ (𝑧 = (𝐴 ∖ 𝑥) → (𝜓 ↔ 𝜒))
fin23lem11.2	⊢ (𝑤 = (𝐴 ∖ 𝑣) → (𝜑 ↔ 𝜃))
fin23lem11.3	⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
fin23lem11	⊢ (𝐵 ⊆ 𝒫 𝐴 → (∃𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓))

Distinct variable groups:   𝑣,𝑐,𝑤,𝑥,𝑧,𝐴   𝐵,𝑐,𝑣,𝑤,𝑥,𝑧   𝜒,𝑧   𝜑,𝑣   𝜓,𝑥   𝜃,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑧,𝑤,𝑐)   𝜓(𝑧,𝑤,𝑣,𝑐)   𝜒(𝑥,𝑤,𝑣,𝑐)   𝜃(𝑥,𝑧,𝑣,𝑐)

Proof of Theorem fin23lem11

Step	Hyp	Ref	Expression
1		difeq2 3918	. . . . 5 ⊢ (𝑐 = 𝑥 → (𝐴 ∖ 𝑐) = (𝐴 ∖ 𝑥))
2	1	eleq1d 2861	. . . 4 ⊢ (𝑐 = 𝑥 → ((𝐴 ∖ 𝑐) ∈ 𝐵 ↔ (𝐴 ∖ 𝑥) ∈ 𝐵))
3	2	elrab 3554	. . 3 ⊢ (𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵))
4		simp2r 1258	. . . . 5 ⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) → (𝐴 ∖ 𝑥) ∈ 𝐵)
5		fin23lem11.2	. . . . . . . . 9 ⊢ (𝑤 = (𝐴 ∖ 𝑣) → (𝜑 ↔ 𝜃))
6	5	notbid 310	. . . . . . . 8 ⊢ (𝑤 = (𝐴 ∖ 𝑣) → (¬ 𝜑 ↔ ¬ 𝜃))
7		simpl3 1247	. . . . . . . 8 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑)
8		difss 3933	. . . . . . . . . 10 ⊢ (𝐴 ∖ 𝑣) ⊆ 𝐴
9		ssun1 3972	. . . . . . . . . . . . 13 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝑥)
10		undif1 4235	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝑥) ∪ 𝑥) = (𝐴 ∪ 𝑥)
11	9, 10	sseqtr4i 3832	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ ((𝐴 ∖ 𝑥) ∪ 𝑥)
12		simpl2r 1300	. . . . . . . . . . . . 13 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ 𝑥) ∈ 𝐵)
13		simpl2l 1298	. . . . . . . . . . . . 13 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑥 ∈ 𝒫 𝐴)
14		unexg 7191	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ 𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝐴 ∖ 𝑥) ∪ 𝑥) ∈ V)
15	12, 13, 14	syl2anc 580	. . . . . . . . . . . 12 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ((𝐴 ∖ 𝑥) ∪ 𝑥) ∈ V)
16		ssexg 4997	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ((𝐴 ∖ 𝑥) ∪ 𝑥) ∧ ((𝐴 ∖ 𝑥) ∪ 𝑥) ∈ V) → 𝐴 ∈ V)
17	11, 15, 16	sylancr 582	. . . . . . . . . . 11 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝐴 ∈ V)
18		elpw2g 5017	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ((𝐴 ∖ 𝑣) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑣) ⊆ 𝐴))
19	17, 18	syl 17	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ((𝐴 ∖ 𝑣) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑣) ⊆ 𝐴))
20	8, 19	mpbiri 250	. . . . . . . . 9 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ 𝑣) ∈ 𝒫 𝐴)
21		simpl1 1243	. . . . . . . . . . . . 13 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝐵 ⊆ 𝒫 𝐴)
22		simpr 478	. . . . . . . . . . . . 13 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵)
23	21, 22	sseldd 3797	. . . . . . . . . . . 12 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝒫 𝐴)
24	23	elpwid 4359	. . . . . . . . . . 11 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑣 ⊆ 𝐴)
25		dfss4 4057	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑣)) = 𝑣)
26	24, 25	sylib 210	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ (𝐴 ∖ 𝑣)) = 𝑣)
27	26, 22	eqeltrd 2876	. . . . . . . . 9 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ (𝐴 ∖ 𝑣)) ∈ 𝐵)
28		difeq2 3918	. . . . . . . . . . 11 ⊢ (𝑐 = (𝐴 ∖ 𝑣) → (𝐴 ∖ 𝑐) = (𝐴 ∖ (𝐴 ∖ 𝑣)))
29	28	eleq1d 2861	. . . . . . . . . 10 ⊢ (𝑐 = (𝐴 ∖ 𝑣) → ((𝐴 ∖ 𝑐) ∈ 𝐵 ↔ (𝐴 ∖ (𝐴 ∖ 𝑣)) ∈ 𝐵))
30	29	elrab 3554	. . . . . . . . 9 ⊢ ((𝐴 ∖ 𝑣) ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ↔ ((𝐴 ∖ 𝑣) ∈ 𝒫 𝐴 ∧ (𝐴 ∖ (𝐴 ∖ 𝑣)) ∈ 𝐵))
31	20, 27, 30	sylanbrc 579	. . . . . . . 8 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ 𝑣) ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵})
32	6, 7, 31	rspcdva 3501	. . . . . . 7 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ¬ 𝜃)
33		simplrl 796	. . . . . . . . . . 11 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑥 ∈ 𝒫 𝐴)
34	33	elpwid 4359	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑥 ⊆ 𝐴)
35		ssel2 3791	. . . . . . . . . . . 12 ⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝒫 𝐴)
36	35	adantlr 707	. . . . . . . . . . 11 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝒫 𝐴)
37	36	elpwid 4359	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ⊆ 𝐴)
38		fin23lem11.3	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) → (𝜒 ↔ 𝜃))
39	34, 37, 38	syl2anc 580	. . . . . . . . 9 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → (𝜒 ↔ 𝜃))
40	39	notbid 310	. . . . . . . 8 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → (¬ 𝜒 ↔ ¬ 𝜃))
41	40	3adantl3 1210	. . . . . . 7 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (¬ 𝜒 ↔ ¬ 𝜃))
42	32, 41	mpbird 249	. . . . . 6 ⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ¬ 𝜒)
43	42	ralrimiva 3145	. . . . 5 ⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) → ∀𝑣 ∈ 𝐵 ¬ 𝜒)
44		fin23lem11.1	. . . . . . . 8 ⊢ (𝑧 = (𝐴 ∖ 𝑥) → (𝜓 ↔ 𝜒))
45	44	notbid 310	. . . . . . 7 ⊢ (𝑧 = (𝐴 ∖ 𝑥) → (¬ 𝜓 ↔ ¬ 𝜒))
46	45	ralbidv 3165	. . . . . 6 ⊢ (𝑧 = (𝐴 ∖ 𝑥) → (∀𝑣 ∈ 𝐵 ¬ 𝜓 ↔ ∀𝑣 ∈ 𝐵 ¬ 𝜒))
47	46	rspcev 3495	. . . . 5 ⊢ (((𝐴 ∖ 𝑥) ∈ 𝐵 ∧ ∀𝑣 ∈ 𝐵 ¬ 𝜒) → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓)
48	4, 43, 47	syl2anc 580	. . . 4 ⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓)
49	48	3exp 1149	. . 3 ⊢ (𝐵 ⊆ 𝒫 𝐴 → ((𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) → (∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓)))
50	3, 49	syl5bi 234	. 2 ⊢ (𝐵 ⊆ 𝒫 𝐴 → (𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} → (∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓)))
51	50	rexlimdv 3209	1 ⊢ (𝐵 ⊆ 𝒫 𝐴 → (∃𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 385   ∧ w3a 1108   = wceq 1653   ∈ wcel 2157  ∀wral 3087  ∃wrex 3088  {crab 3091  Vcvv 3383   ∖ cdif 3764   ∪ cun 3765   ⊆ wss 3767  𝒫 cpw 4347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pr 5095  ax-un 7181

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-pw 4349  df-sn 4367  df-pr 4369  df-uni 4627

This theorem is referenced by:  fin2i2  9426  isfin2-2  9427