Metamath Proof Explorer

Theorem fin1a2lem10

Description: Lemma for fin1a2 . A nonempty finite union of members of a chain is a member of the chain. (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem10 ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [⊊] Or 𝐴 ) → ∪ 𝐴 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 eqneqall ⊢ ( 𝑎 = ∅ → ( 𝑎 ≠ ∅ → ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ) )
2 tru ⊢ ⊤
3 2 a1i ⊢ ( 𝑎 = ∅ → ⊤ )
4 1 3 2thd ⊢ ( 𝑎 = ∅ → ( ( 𝑎 ≠ ∅ → ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ) ↔ ⊤ ) )
5 neeq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ≠ ∅ ↔ 𝑏 ≠ ∅ ) )
6 soeq2 ⊢ ( 𝑎 = 𝑏 → ( [⊊] Or 𝑎 ↔ [⊊] Or 𝑏 ) )
7 unieq ⊢ ( 𝑎 = 𝑏 → ∪ 𝑎 = ∪ 𝑏 )
8 id ⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
9 7 8 eleq12d ⊢ ( 𝑎 = 𝑏 → ( ∪ 𝑎 ∈ 𝑎 ↔ ∪ 𝑏 ∈ 𝑏 ) )
10 6 9 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ↔ ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) )
11 5 10 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ≠ ∅ → ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ) ↔ ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) ) )
12 neeq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎 ≠ ∅ ↔ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) )
13 soeq2 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( [⊊] Or 𝑎 ↔ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ) )
14 unieq ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ∪ 𝑎 = ∪ ( 𝑏 ∪ { 𝑐 } ) )
15 id ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → 𝑎 = ( 𝑏 ∪ { 𝑐 } ) )
16 14 15 eleq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ∪ 𝑎 ∈ 𝑎 ↔ ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
17 13 16 imbi12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ↔ ( [⊊] Or ( 𝑏 ∪ { 𝑐 } ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) ) )
18 12 17 imbi12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑎 ≠ ∅ → ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ) ↔ ( ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ → ( [⊊] Or ( 𝑏 ∪ { 𝑐 } ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) ) ) )
19 neeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
20 soeq2 ⊢ ( 𝑎 = 𝐴 → ( [⊊] Or 𝑎 ↔ [⊊] Or 𝐴 ) )
21 unieq ⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴 )
22 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
23 21 22 eleq12d ⊢ ( 𝑎 = 𝐴 → ( ∪ 𝑎 ∈ 𝑎 ↔ ∪ 𝐴 ∈ 𝐴 ) )
24 20 23 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ↔ ( [⊊] Or 𝐴 → ∪ 𝐴 ∈ 𝐴 ) ) )
25 19 24 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ≠ ∅ → ( [⊊] Or 𝑎 → ∪ 𝑎 ∈ 𝑎 ) ) ↔ ( 𝐴 ≠ ∅ → ( [⊊] Or 𝐴 → ∪ 𝐴 ∈ 𝐴 ) ) ) )
26 unisnv ⊢ ∪ { 𝑐 } = 𝑐
27 vsnid ⊢ 𝑐 ∈ { 𝑐 }
28 26 27 eqeltri ⊢ ∪ { 𝑐 } ∈ { 𝑐 }
29 uneq1 ⊢ ( 𝑏 = ∅ → ( 𝑏 ∪ { 𝑐 } ) = ( ∅ ∪ { 𝑐 } ) )
30 uncom ⊢ ( ∅ ∪ { 𝑐 } ) = ( { 𝑐 } ∪ ∅ )
31 un0 ⊢ ( { 𝑐 } ∪ ∅ ) = { 𝑐 }
32 30 31 eqtri ⊢ ( ∅ ∪ { 𝑐 } ) = { 𝑐 }
33 29 32 eqtrdi ⊢ ( 𝑏 = ∅ → ( 𝑏 ∪ { 𝑐 } ) = { 𝑐 } )
34 33 unieqd ⊢ ( 𝑏 = ∅ → ∪ ( 𝑏 ∪ { 𝑐 } ) = ∪ { 𝑐 } )
35 34 33 eleq12d ⊢ ( 𝑏 = ∅ → ( ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ↔ ∪ { 𝑐 } ∈ { 𝑐 } ) )
36 28 35 mpbiri ⊢ ( 𝑏 = ∅ → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
37 36 a1d ⊢ ( 𝑏 = ∅ → ( ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
38 37 adantl ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 = ∅ ) → ( ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
39 simpr ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 ≠ ∅ ) → 𝑏 ≠ ∅ )
40 ssun1 ⊢ 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } )
41 simpl2 ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 ≠ ∅ ) → [⊊] Or ( 𝑏 ∪ { 𝑐 } ) )
42 soss ⊢ ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } ) → ( [⊊] Or ( 𝑏 ∪ { 𝑐 } ) → [⊊] Or 𝑏 ) )
43 40 41 42 mpsyl ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 ≠ ∅ ) → [⊊] Or 𝑏 )
44 uniun ⊢ ∪ ( 𝑏 ∪ { 𝑐 } ) = ( ∪ 𝑏 ∪ ∪ { 𝑐 } )
45 26 uneq2i ⊢ ( ∪ 𝑏 ∪ ∪ { 𝑐 } ) = ( ∪ 𝑏 ∪ 𝑐 )
46 44 45 eqtri ⊢ ∪ ( 𝑏 ∪ { 𝑐 } ) = ( ∪ 𝑏 ∪ 𝑐 )
47 simprr ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → ∪ 𝑏 ∈ 𝑏 )
48 simpl2 ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → [⊊] Or ( 𝑏 ∪ { 𝑐 } ) )
49 elun1 ⊢ ( ∪ 𝑏 ∈ 𝑏 → ∪ 𝑏 ∈ ( 𝑏 ∪ { 𝑐 } ) )
50 49 ad2antll ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → ∪ 𝑏 ∈ ( 𝑏 ∪ { 𝑐 } ) )
51 ssun2 ⊢ { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } )
52 51 27 sselii ⊢ 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } )
53 52 a1i ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) )
54 sorpssi ⊢ ( ( [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( ∪ 𝑏 ∈ ( 𝑏 ∪ { 𝑐 } ) ∧ 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) ) ) → ( ∪ 𝑏 ⊆ 𝑐 ∨ 𝑐 ⊆ ∪ 𝑏 ) )
55 48 50 53 54 syl12anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → ( ∪ 𝑏 ⊆ 𝑐 ∨ 𝑐 ⊆ ∪ 𝑏 ) )
56 ssequn1 ⊢ ( ∪ 𝑏 ⊆ 𝑐 ↔ ( ∪ 𝑏 ∪ 𝑐 ) = 𝑐 )
57 52 a1i ⊢ ( ∪ 𝑏 ∈ 𝑏 → 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) )
58 eleq1 ⊢ ( ( ∪ 𝑏 ∪ 𝑐 ) = 𝑐 → ( ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) ↔ 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
59 57 58 imbitrrid ⊢ ( ( ∪ 𝑏 ∪ 𝑐 ) = 𝑐 → ( ∪ 𝑏 ∈ 𝑏 → ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
60 56 59 sylbi ⊢ ( ∪ 𝑏 ⊆ 𝑐 → ( ∪ 𝑏 ∈ 𝑏 → ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
61 60 impcom ⊢ ( ( ∪ 𝑏 ∈ 𝑏 ∧ ∪ 𝑏 ⊆ 𝑐 ) → ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
62 uncom ⊢ ( ∪ 𝑏 ∪ 𝑐 ) = ( 𝑐 ∪ ∪ 𝑏 )
63 ssequn1 ⊢ ( 𝑐 ⊆ ∪ 𝑏 ↔ ( 𝑐 ∪ ∪ 𝑏 ) = ∪ 𝑏 )
64 eleq1 ⊢ ( ( 𝑐 ∪ ∪ 𝑏 ) = ∪ 𝑏 → ( ( 𝑐 ∪ ∪ 𝑏 ) ∈ ( 𝑏 ∪ { 𝑐 } ) ↔ ∪ 𝑏 ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
65 49 64 imbitrrid ⊢ ( ( 𝑐 ∪ ∪ 𝑏 ) = ∪ 𝑏 → ( ∪ 𝑏 ∈ 𝑏 → ( 𝑐 ∪ ∪ 𝑏 ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
66 63 65 sylbi ⊢ ( 𝑐 ⊆ ∪ 𝑏 → ( ∪ 𝑏 ∈ 𝑏 → ( 𝑐 ∪ ∪ 𝑏 ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
67 66 impcom ⊢ ( ( ∪ 𝑏 ∈ 𝑏 ∧ 𝑐 ⊆ ∪ 𝑏 ) → ( 𝑐 ∪ ∪ 𝑏 ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
68 62 67 eqeltrid ⊢ ( ( ∪ 𝑏 ∈ 𝑏 ∧ 𝑐 ⊆ ∪ 𝑏 ) → ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
69 61 68 jaodan ⊢ ( ( ∪ 𝑏 ∈ 𝑏 ∧ ( ∪ 𝑏 ⊆ 𝑐 ∨ 𝑐 ⊆ ∪ 𝑏 ) ) → ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
70 47 55 69 syl2anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → ( ∪ 𝑏 ∪ 𝑐 ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
71 46 70 eqeltrid ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ ( 𝑏 ≠ ∅ ∧ ∪ 𝑏 ∈ 𝑏 ) ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) )
72 71 expr ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 ≠ ∅ ) → ( ∪ 𝑏 ∈ 𝑏 → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
73 43 72 embantd ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 ≠ ∅ ) → ( ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
74 39 73 embantd ⊢ ( ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) ∧ 𝑏 ≠ ∅ ) → ( ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
75 38 74 pm2.61dane ⊢ ( ( 𝑏 ∈ Fin ∧ [⊊] Or ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ ) → ( ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) )
76 75 3exp ⊢ ( 𝑏 ∈ Fin → ( [⊊] Or ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ → ( ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) ) ) )
77 76 com24 ⊢ ( 𝑏 ∈ Fin → ( ( 𝑏 ≠ ∅ → ( [⊊] Or 𝑏 → ∪ 𝑏 ∈ 𝑏 ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ≠ ∅ → ( [⊊] Or ( 𝑏 ∪ { 𝑐 } ) → ∪ ( 𝑏 ∪ { 𝑐 } ) ∈ ( 𝑏 ∪ { 𝑐 } ) ) ) ) )
78 4 11 18 25 2 77 findcard2 ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≠ ∅ → ( [⊊] Or 𝐴 → ∪ 𝐴 ∈ 𝐴 ) ) )
79 78 3imp21 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [⊊] Or 𝐴 ) → ∪ 𝐴 ∈ 𝐴 )