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 X ∧ X ⊆ Fin ∧ A ∈ ω → b ∈ X | b ≼ A ∈ Fin

Proof

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