Theorem isfin4p1

Description: Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 can be assumed to be only a singleton smaller than the original.) (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	isfin4p1	⊢ ( 𝐴 ∈ FinIV ↔ 𝐴 ≺ ( 𝐴 ⊔ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1o ∈ On
2		djudoml	⊢ ( ( 𝐴 ∈ FinIV ∧ 1o ∈ On ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ FinIV → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
4		1oex	⊢ 1o ∈ V
5	4	snid	⊢ 1o ∈ { 1o }
6		0lt1o	⊢ ∅ ∈ 1o
7		opelxpi	⊢ ( ( 1o ∈ { 1o } ∧ ∅ ∈ 1o ) → ⟨ 1o , ∅ ⟩ ∈ ( { 1o } × 1o ) )
8	5 6 7	mp2an	⊢ ⟨ 1o , ∅ ⟩ ∈ ( { 1o } × 1o )
9		elun2	⊢ ( ⟨ 1o , ∅ ⟩ ∈ ( { 1o } × 1o ) → ⟨ 1o , ∅ ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) )
10	8 9	ax-mp	⊢ ⟨ 1o , ∅ ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
11		df-dju	⊢ ( 𝐴 ⊔ 1o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
12	10 11	eleqtrri	⊢ ⟨ 1o , ∅ ⟩ ∈ ( 𝐴 ⊔ 1o )
13		1n0	⊢ 1o ≠ ∅
14		opelxp1	⊢ ( ⟨ 1o , ∅ ⟩ ∈ ( { ∅ } × 𝐴 ) → 1o ∈ { ∅ } )
15		elsni	⊢ ( 1o ∈ { ∅ } → 1o = ∅ )
16	14 15	syl	⊢ ( ⟨ 1o , ∅ ⟩ ∈ ( { ∅ } × 𝐴 ) → 1o = ∅ )
17	16	necon3ai	⊢ ( 1o ≠ ∅ → ¬ ⟨ 1o , ∅ ⟩ ∈ ( { ∅ } × 𝐴 ) )
18	13 17	ax-mp	⊢ ¬ ⟨ 1o , ∅ ⟩ ∈ ( { ∅ } × 𝐴 )
19		ssun1	⊢ ( { ∅ } × 𝐴 ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
20	19 11	sseqtrri	⊢ ( { ∅ } × 𝐴 ) ⊆ ( 𝐴 ⊔ 1o )
21		ssnelpss	⊢ ( ( { ∅ } × 𝐴 ) ⊆ ( 𝐴 ⊔ 1o ) → ( ( ⟨ 1o , ∅ ⟩ ∈ ( 𝐴 ⊔ 1o ) ∧ ¬ ⟨ 1o , ∅ ⟩ ∈ ( { ∅ } × 𝐴 ) ) → ( { ∅ } × 𝐴 ) ⊊ ( 𝐴 ⊔ 1o ) ) )
22	20 21	ax-mp	⊢ ( ( ⟨ 1o , ∅ ⟩ ∈ ( 𝐴 ⊔ 1o ) ∧ ¬ ⟨ 1o , ∅ ⟩ ∈ ( { ∅ } × 𝐴 ) ) → ( { ∅ } × 𝐴 ) ⊊ ( 𝐴 ⊔ 1o ) )
23	12 18 22	mp2an	⊢ ( { ∅ } × 𝐴 ) ⊊ ( 𝐴 ⊔ 1o )
24		0ex	⊢ ∅ ∈ V
25		relen	⊢ Rel ≈
26	25	brrelex1i	⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 1o ) → 𝐴 ∈ V )
27		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
28	24 26 27	sylancr	⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 1o ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
29		entr	⊢ ( ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≈ ( 𝐴 ⊔ 1o ) ) → ( { ∅ } × 𝐴 ) ≈ ( 𝐴 ⊔ 1o ) )
30	28 29	mpancom	⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 1o ) → ( { ∅ } × 𝐴 ) ≈ ( 𝐴 ⊔ 1o ) )
31		fin4i	⊢ ( ( ( { ∅ } × 𝐴 ) ⊊ ( 𝐴 ⊔ 1o ) ∧ ( { ∅ } × 𝐴 ) ≈ ( 𝐴 ⊔ 1o ) ) → ¬ ( 𝐴 ⊔ 1o ) ∈ FinIV )
32	23 30 31	sylancr	⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 1o ) → ¬ ( 𝐴 ⊔ 1o ) ∈ FinIV )
33		fin4en1	⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 1o ) → ( 𝐴 ∈ FinIV → ( 𝐴 ⊔ 1o ) ∈ FinIV ) )
34	32 33	mtod	⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 1o ) → ¬ 𝐴 ∈ FinIV )
35	34	con2i	⊢ ( 𝐴 ∈ FinIV → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
36		brsdom	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) ↔ ( 𝐴 ≼ ( 𝐴 ⊔ 1o ) ∧ ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) ) )
37	3 35 36	sylanbrc	⊢ ( 𝐴 ∈ FinIV → 𝐴 ≺ ( 𝐴 ⊔ 1o ) )
38		sdomnen	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
39		infdju1	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
40	39	ensymd	⊢ ( ω ≼ 𝐴 → 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
41	38 40	nsyl	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → ¬ ω ≼ 𝐴 )
42		relsdom	⊢ Rel ≺
43	42	brrelex1i	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → 𝐴 ∈ V )
44		isfin4-2	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) )
45	43 44	syl	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) )
46	41 45	mpbird	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → 𝐴 ∈ FinIV )
47	37 46	impbii	⊢ ( 𝐴 ∈ FinIV ↔ 𝐴 ≺ ( 𝐴 ⊔ 1o ) )