ssfin4

Description: Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 6-May-2015) (Revised by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	ssfin4	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin^IV )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → 𝐴 ∈ Fin^IV )
2		pssss	⊢ ( 𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵 )
3		simpr	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
4	2 3	sylan9ssr	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) → 𝑥 ⊆ 𝐴 )
5		difssd	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
6	4 5	unssd	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ⊆ 𝐴 )
7		pssnel	⊢ ( 𝑥 ⊊ 𝐵 → ∃ 𝑐 ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) → ∃ 𝑐 ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) )
9		simpllr	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → 𝐵 ⊆ 𝐴 )
10		simprl	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → 𝑐 ∈ 𝐵 )
11	9 10	sseldd	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → 𝑐 ∈ 𝐴 )
12		simprr	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → ¬ 𝑐 ∈ 𝑥 )
13		elndif	⊢ ( 𝑐 ∈ 𝐵 → ¬ 𝑐 ∈ ( 𝐴 ∖ 𝐵 ) )
14	13	ad2antrl	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → ¬ 𝑐 ∈ ( 𝐴 ∖ 𝐵 ) )
15		ioran	⊢ ( ¬ ( 𝑐 ∈ 𝑥 ∨ 𝑐 ∈ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ¬ 𝑐 ∈ 𝑥 ∧ ¬ 𝑐 ∈ ( 𝐴 ∖ 𝐵 ) ) )
16		elun	⊢ ( 𝑐 ∈ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝑐 ∈ 𝑥 ∨ 𝑐 ∈ ( 𝐴 ∖ 𝐵 ) ) )
17	15 16	xchnxbir	⊢ ( ¬ 𝑐 ∈ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ¬ 𝑐 ∈ 𝑥 ∧ ¬ 𝑐 ∈ ( 𝐴 ∖ 𝐵 ) ) )
18	12 14 17	sylanbrc	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → ¬ 𝑐 ∈ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) )
19		nelneq2	⊢ ( ( 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ) → ¬ 𝐴 = ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) )
20	11 18 19	syl2anc	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → ¬ 𝐴 = ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) )
21		eqcom	⊢ ( 𝐴 = ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
22	20 21	sylnib	⊢ ( ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ ( 𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥 ) ) → ¬ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
23	8 22	exlimddv	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) → ¬ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
24		dfpss2	⊢ ( ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ⊊ 𝐴 ↔ ( ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ⊆ 𝐴 ∧ ¬ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 ) )
25	6 23 24	sylanbrc	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ⊊ 𝐴 )
26	25	adantrr	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ⊊ 𝐴 )
27		simprr	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → 𝑥 ≈ 𝐵 )
28		difexg	⊢ ( 𝐴 ∈ Fin^IV → ( 𝐴 ∖ 𝐵 ) ∈ V )
29		enrefg	⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ V → ( 𝐴 ∖ 𝐵 ) ≈ ( 𝐴 ∖ 𝐵 ) )
30	1 28 29	3syl	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝐴 ∖ 𝐵 ) ≈ ( 𝐴 ∖ 𝐵 ) )
31	2	ad2antrl	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → 𝑥 ⊆ 𝐵 )
32		ssinss1	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐵 )
33	31 32	syl	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐵 )
34		inssdif0	⊢ ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝐵 ↔ ( 𝑥 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ )
35	33 34	sylib	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑥 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ )
36		disjdif	⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
37	35 36	jctir	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( ( 𝑥 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ∧ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ) )
38		unen	⊢ ( ( ( 𝑥 ≈ 𝐵 ∧ ( 𝐴 ∖ 𝐵 ) ≈ ( 𝐴 ∖ 𝐵 ) ) ∧ ( ( 𝑥 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ∧ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ) ) → ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ≈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
39	27 30 37 38	syl21anc	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ≈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
40		simplr	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → 𝐵 ⊆ 𝐴 )
41		undif	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
42	40 41	sylib	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
43	39 42	breqtrd	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ≈ 𝐴 )
44		fin4i	⊢ ( ( ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ⊊ 𝐴 ∧ ( 𝑥 ∪ ( 𝐴 ∖ 𝐵 ) ) ≈ 𝐴 ) → ¬ 𝐴 ∈ Fin^IV )
45	26 43 44	syl2anc	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ¬ 𝐴 ∈ Fin^IV )
46	1 45	pm2.65da	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → ¬ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) )
47	46	nexdv	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) )
48		ssexg	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin^IV ) → 𝐵 ∈ V )
49	48	ancoms	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V )
50		isfin4	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin^IV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
51	49 50	syl	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ∈ Fin^IV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
52	47 51	mpbird	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin^IV )

Metamath Proof Explorer

Theorem ssfin4

Proof