This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 0fi ⊢ ∅ ∈ 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 vsnex ⊢ { 𝑑 } ∈ 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 biimtrid ⊢ ( ( 𝑏 ∈ ( 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 𝒫 𝐴 ) )