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 syl5bi ( ( [] 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 )