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

Metamath Proof Explorer

Theorem fin1a2lem9

Description: Lemma for fin1a2 . In a chain of finite sets, initial segments are finite. (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem9 ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∈ Fin )

Proof

Step Hyp Ref Expression
1 onfin2 ⊢ ω = ( On ∩ Fin )
2 inss2 ⊢ ( On ∩ Fin ) ⊆ Fin
3 1 2 eqsstri ⊢ ω ⊆ Fin
4 peano2 ⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
5 3 4 sselid ⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ Fin )
6 5 3ad2ant3 ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → suc 𝐴 ∈ Fin )
7 4 3ad2ant3 ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → suc 𝐴 ∈ ω )
8 breq1 ⊢ ( 𝑏 = 𝑐 → ( 𝑏 ≼ 𝐴 ↔ 𝑐 ≼ 𝐴 ) )
9 8 elrab ⊢ ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ↔ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) )
10 simprr ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ≼ 𝐴 )
11 simpl2 ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑋 ⊆ Fin )
12 simprl ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ∈ 𝑋 )
13 11 12 sseldd ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ∈ Fin )
14 finnum ⊢ ( 𝑐 ∈ Fin → 𝑐 ∈ dom card )
15 13 14 syl ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ∈ dom card )
16 simpl3 ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝐴 ∈ ω )
17 3 16 sselid ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝐴 ∈ Fin )
18 finnum ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
19 17 18 syl ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝐴 ∈ dom card )
20 carddom2 ⊢ ( ( 𝑐 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ 𝑐 ≼ 𝐴 ) )
21 15 19 20 syl2anc ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ 𝑐 ≼ 𝐴 ) )
22 10 21 mpbird ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) )
23 22 ex ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) → ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ) )
24 cardnn ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝐴 ) = 𝐴 )
25 24 sseq2d ⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝑐 ) ⊆ 𝐴 ) )
26 cardon ⊢ ( card ‘ 𝑐 ) ∈ On
27 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
28 onsssuc ⊢ ( ( ( card ‘ 𝑐 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( card ‘ 𝑐 ) ⊆ 𝐴 ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) )
29 26 27 28 sylancr ⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝑐 ) ⊆ 𝐴 ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) )
30 25 29 bitrd ⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) )
31 30 3ad2ant3 ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) )
32 23 31 sylibd ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) → ( card ‘ 𝑐 ) ∈ suc 𝐴 ) )
33 9 32 biimtrid ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } → ( card ‘ 𝑐 ) ∈ suc 𝐴 ) )
34 elrabi ⊢ ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } → 𝑐 ∈ 𝑋 )
35 elrabi ⊢ ( 𝑑 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } → 𝑑 ∈ 𝑋 )
36 ssel ⊢ ( 𝑋 ⊆ Fin → ( 𝑐 ∈ 𝑋 → 𝑐 ∈ Fin ) )
37 ssel ⊢ ( 𝑋 ⊆ Fin → ( 𝑑 ∈ 𝑋 → 𝑑 ∈ Fin ) )
38 36 37 anim12d ⊢ ( 𝑋 ⊆ Fin → ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) → ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ) )
39 38 imp ⊢ ( ( 𝑋 ⊆ Fin ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) )
40 39 3ad2antl2 ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) )
41 sorpssi ⊢ ( ( [⊊] Or 𝑋 ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) )
42 41 3ad2antl1 ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) )
43 finnum ⊢ ( 𝑑 ∈ Fin → 𝑑 ∈ dom card )
44 carden2 ⊢ ( ( 𝑐 ∈ dom card ∧ 𝑑 ∈ dom card ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 ≈ 𝑑 ) )
45 14 43 44 syl2an ⊢ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 ≈ 𝑑 ) )
46 45 adantr ⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 ≈ 𝑑 ) )
47 fin23lem25 ⊢ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( 𝑐 ≈ 𝑑 ↔ 𝑐 = 𝑑 ) )
48 47 3expa ⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( 𝑐 ≈ 𝑑 ↔ 𝑐 = 𝑑 ) )
49 48 biimpd ⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( 𝑐 ≈ 𝑑 → 𝑐 = 𝑑 ) )
50 46 49 sylbid ⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
51 40 42 50 syl2anc ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
52 fveq2 ⊢ ( 𝑐 = 𝑑 → ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) )
53 51 52 impbid1 ⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) )
54 53 ex ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) ) )
55 34 35 54 syl2ani ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∧ 𝑑 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) ) )
56 33 55 dom2d ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( suc 𝐴 ∈ ω → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ≼ suc 𝐴 ) )
57 7 56 mpd ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ≼ suc 𝐴 )
58 domfi ⊢ ( ( suc 𝐴 ∈ Fin ∧ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ≼ suc 𝐴 ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∈ Fin )
59 6 57 58 syl2anc ⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∈ Fin )