Theorem isfin1-3

Description: A set is I-finite iff every system of subsets contains a maximal subset. Definition I of Levy58 p. 2. (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin1-3	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ ◡ [⊊] Fr 𝒫 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		porpss	⊢ [⊊] Po 𝒫 𝐴
2		cnvpo	⊢ ( [⊊] Po 𝒫 𝐴 ↔ ◡ [⊊] Po 𝒫 𝐴 )
3	1 2	mpbi	⊢ ◡ [⊊] Po 𝒫 𝐴
4		pwfi	⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
5	4	biimpi	⊢ ( 𝐴 ∈ Fin → 𝒫 𝐴 ∈ Fin )
6		frfi	⊢ ( ( ◡ [⊊] Po 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ Fin ) → ◡ [⊊] Fr 𝒫 𝐴 )
7	3 5 6	sylancr	⊢ ( 𝐴 ∈ Fin → ◡ [⊊] Fr 𝒫 𝐴 )
8		inss2	⊢ ( Fin ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴
9		pwexg	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
10		ssexg	⊢ ( ( ( Fin ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V ) → ( Fin ∩ 𝒫 𝐴 ) ∈ V )
11	8 9 10	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( Fin ∩ 𝒫 𝐴 ) ∈ V )
12		0fin	⊢ ∅ ∈ Fin
13		0elpw	⊢ ∅ ∈ 𝒫 𝐴
14	12 13	elini	⊢ ∅ ∈ ( Fin ∩ 𝒫 𝐴 )
15	14	ne0ii	⊢ ( Fin ∩ 𝒫 𝐴 ) ≠ ∅
16		fri	⊢ ( ( ( ( Fin ∩ 𝒫 𝐴 ) ∈ V ∧ ◡ [⊊] Fr 𝒫 𝐴 ) ∧ ( ( Fin ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ∧ ( Fin ∩ 𝒫 𝐴 ) ≠ ∅ ) ) → ∃ 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 )
17	8 15 16	mpanr12	⊢ ( ( ( Fin ∩ 𝒫 𝐴 ) ∈ V ∧ ◡ [⊊] Fr 𝒫 𝐴 ) → ∃ 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 )
18	11 17	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ◡ [⊊] Fr 𝒫 𝐴 ) → ∃ 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 )
19	18	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ [⊊] Fr 𝒫 𝐴 → ∃ 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 ) )
20		elinel1	⊢ ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) → 𝑏 ∈ Fin )
21		ralnex	⊢ ( ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 ↔ ¬ ∃ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) 𝑐 ◡ [⊊] 𝑏 )
22	20	adantr	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → 𝑏 ∈ Fin )
23		snfi	⊢ { 𝑑 } ∈ Fin
24		unfi	⊢ ( ( 𝑏 ∈ Fin ∧ { 𝑑 } ∈ Fin ) → ( 𝑏 ∪ { 𝑑 } ) ∈ Fin )
25	22 23 24	sylancl	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → ( 𝑏 ∪ { 𝑑 } ) ∈ Fin )
26		elinel2	⊢ ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) → 𝑏 ∈ 𝒫 𝐴 )
27	26	elpwid	⊢ ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) → 𝑏 ⊆ 𝐴 )
28	27	adantr	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → 𝑏 ⊆ 𝐴 )
29		snssi	⊢ ( 𝑑 ∈ 𝐴 → { 𝑑 } ⊆ 𝐴 )
30	29	ad2antrl	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → { 𝑑 } ⊆ 𝐴 )
31	28 30	unssd	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → ( 𝑏 ∪ { 𝑑 } ) ⊆ 𝐴 )
32		vex	⊢ 𝑏 ∈ V
33		snex	⊢ { 𝑑 } ∈ V
34	32 33	unex	⊢ ( 𝑏 ∪ { 𝑑 } ) ∈ V
35	34	elpw	⊢ ( ( 𝑏 ∪ { 𝑑 } ) ∈ 𝒫 𝐴 ↔ ( 𝑏 ∪ { 𝑑 } ) ⊆ 𝐴 )
36	31 35	sylibr	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → ( 𝑏 ∪ { 𝑑 } ) ∈ 𝒫 𝐴 )
37	25 36	elind	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → ( 𝑏 ∪ { 𝑑 } ) ∈ ( Fin ∩ 𝒫 𝐴 ) )
38		disjsn	⊢ ( ( 𝑏 ∩ { 𝑑 } ) = ∅ ↔ ¬ 𝑑 ∈ 𝑏 )
39	38	biimpri	⊢ ( ¬ 𝑑 ∈ 𝑏 → ( 𝑏 ∩ { 𝑑 } ) = ∅ )
40		vex	⊢ 𝑑 ∈ V
41	40	snnz	⊢ { 𝑑 } ≠ ∅
42		disjpss	⊢ ( ( ( 𝑏 ∩ { 𝑑 } ) = ∅ ∧ { 𝑑 } ≠ ∅ ) → 𝑏 ⊊ ( 𝑏 ∪ { 𝑑 } ) )
43	39 41 42	sylancl	⊢ ( ¬ 𝑑 ∈ 𝑏 → 𝑏 ⊊ ( 𝑏 ∪ { 𝑑 } ) )
44	43	ad2antll	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → 𝑏 ⊊ ( 𝑏 ∪ { 𝑑 } ) )
45	34 32	brcnv	⊢ ( ( 𝑏 ∪ { 𝑑 } ) ◡ [⊊] 𝑏 ↔ 𝑏 [⊊] ( 𝑏 ∪ { 𝑑 } ) )
46	34	brrpss	⊢ ( 𝑏 [⊊] ( 𝑏 ∪ { 𝑑 } ) ↔ 𝑏 ⊊ ( 𝑏 ∪ { 𝑑 } ) )
47	45 46	bitri	⊢ ( ( 𝑏 ∪ { 𝑑 } ) ◡ [⊊] 𝑏 ↔ 𝑏 ⊊ ( 𝑏 ∪ { 𝑑 } ) )
48	44 47	sylibr	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → ( 𝑏 ∪ { 𝑑 } ) ◡ [⊊] 𝑏 )
49		breq1	⊢ ( 𝑐 = ( 𝑏 ∪ { 𝑑 } ) → ( 𝑐 ◡ [⊊] 𝑏 ↔ ( 𝑏 ∪ { 𝑑 } ) ◡ [⊊] 𝑏 ) )
50	49	rspcev	⊢ ( ( ( 𝑏 ∪ { 𝑑 } ) ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑏 ∪ { 𝑑 } ) ◡ [⊊] 𝑏 ) → ∃ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) 𝑐 ◡ [⊊] 𝑏 )
51	37 48 50	syl2anc	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏 ) ) → ∃ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) 𝑐 ◡ [⊊] 𝑏 )
52	51	expr	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ 𝑑 ∈ 𝐴 ) → ( ¬ 𝑑 ∈ 𝑏 → ∃ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) 𝑐 ◡ [⊊] 𝑏 ) )
53	52	con1d	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ 𝑑 ∈ 𝐴 ) → ( ¬ ∃ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) 𝑐 ◡ [⊊] 𝑏 → 𝑑 ∈ 𝑏 ) )
54	21 53	syl5bi	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ 𝑑 ∈ 𝐴 ) → ( ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 → 𝑑 ∈ 𝑏 ) )
55	54	impancom	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 ) → ( 𝑑 ∈ 𝐴 → 𝑑 ∈ 𝑏 ) )
56	55	ssrdv	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 ) → 𝐴 ⊆ 𝑏 )
57		ssfi	⊢ ( ( 𝑏 ∈ Fin ∧ 𝐴 ⊆ 𝑏 ) → 𝐴 ∈ Fin )
58	20 56 57	syl2an2r	⊢ ( ( 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 ) → 𝐴 ∈ Fin )
59	58	rexlimiva	⊢ ( ∃ 𝑏 ∈ ( Fin ∩ 𝒫 𝐴 ) ∀ 𝑐 ∈ ( Fin ∩ 𝒫 𝐴 ) ¬ 𝑐 ◡ [⊊] 𝑏 → 𝐴 ∈ Fin )
60	19 59	syl6	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ [⊊] Fr 𝒫 𝐴 → 𝐴 ∈ Fin ) )
61	7 60	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ ◡ [⊊] Fr 𝒫 𝐴 ) )